eisenstein_successor_row_split_prefix_exists

Proof neighborhood

Direct dependencies

Direct dependents

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. 0007induction l
8. 0008intro hchoices
9. 0009exists 0
10. 0010exists 0
11. 0011exists 0
12. 0012exists 0
13. 0013intro i
14. 0014intro hi
15. 0015exfalso
16. 0016cases hi
17. 0017have hsi : S i = 0
18. 0018specialize add_eq_zero_right x
19. 0019specialize add_eq_zero_right (S i)
20. 0020apply add_eq_zero_right
21. 0021exact hi_witness
22. 0022specialize succ_ne_zero i
23. 0023apply succ_ne_zero
24. 0024exact hsi
25. 0025intro hchoices
26. 0026have hprevious_choices : forall efrd_row_index_fubini_row_split_exists_previous. (exists efrd_lt_gap_fubini_row_split_exists_previous_bound. efrd_lt_gap_fubini_row_split_exists_previous_bound + S (efrd_row_index_fubini_row_split_exists_previous) = l) -> exists efrd_count_fubini_row_split_exists_previous efrd_reduced_count_fubini_row_split_exists_previous efrd_terminal_bit_fubini_row_split_exists_previous. ((((exists ff_h_efrd_fubini_row_split_exists_previous_outer_entry. ff_h_efrd_fubini_row_split_exists_previous_outer_entry + S (efrd_count_fubini_row_split_exists_previous) = S ((S (efrd_row_index_fubini_row_split_exists_previous)) * bc)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_outer_entry. bb = ff_q_efrd_fubini_row_split_exists_previous_outer_entry * S ((S (efrd_row_index_fubini_row_split_exists_previous)) * bc) + (efrd_count_fubini_row_split_exists_previous))) /\ (exists efrd_row_code_fubini_row_split_exists_previous_split efrd_row_scale_fubini_row_split_exists_previous_split. (((((forall eri_column_efrd_fubini_row_split_exists_previous_split_successor_prefix. (exists eri_gap_efrd_fubini_row_split_exists_previous_split_successor_prefix_bound. eri_gap_efrd_fubini_row_split_exists_previous_split_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_exists_previous_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_exists_previous_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_exists_previous_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_exists_previous_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_exists_previous_split_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_exists_previous_split_successor_prefix)) * efrd_row_scale_fubini_row_split_exists_previous_split)) /\ exists ff_q_eri_efrd_fubini_row_split_exists_previous_split_successor_prefix_decoded. efrd_row_code_fubini_row_split_exists_previous_split = ff_q_eri_efrd_fubini_row_split_exists_previous_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_exists_previous_split_successor_prefix)) * efrd_row_scale_fubini_row_split_exists_previous_split) + (eri_bit_efrd_fubini_row_split_exists_previous_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_exists_previous_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_exists_previous_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_previous_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_previous) = p * S eri_column_efrd_fubini_row_split_exists_previous_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_previous_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_previous_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_previous_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_exists_previous))) \/ (eri_bit_efrd_fubini_row_split_exists_previous_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_exists_previous_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_previous_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_previous_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_exists_previous) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_previous_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_previous_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_previous) = p * S eri_column_efrd_fubini_row_split_exists_previous_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_exists_previous_split_successor_count_sum ff_v_efrd_fubini_row_split_exists_previous_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_previous_split_successor_count_sum_start. ff_h_efrd_fubini_row_split_exists_previous_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_exists_previous_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_split_successor_count_sum_start. ff_u_efrd_fubini_row_split_exists_previous_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_previous_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_exists_previous_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_previous_split_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_exists_previous_split_successor_count_sum_terminal + S (efrd_count_fubini_row_split_exists_previous) = S ((S (sh)) * ff_v_efrd_fubini_row_split_exists_previous_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_split_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_exists_previous_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_previous_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_exists_previous_split_successor_count_sum) + (efrd_count_fubini_row_split_exists_previous))) /\ forall ff_i_efrd_fubini_row_split_exists_previous_split_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_exists_previous_split_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_exists_previous_split_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_exists_previous_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_exists_previous_split_successor_count_sum ff_r_efrd_fubini_row_split_exists_previous_split_successor_count_sum ff_s_efrd_fubini_row_split_exists_previous_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_previous_split_successor_count_sum_summand. ff_h_efrd_fubini_row_split_exists_previous_split_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_exists_previous_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_previous_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_exists_previous_split)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_split_successor_count_sum_summand. efrd_row_code_fubini_row_split_exists_previous_split = ff_q_efrd_fubini_row_split_exists_previous_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_exists_previous_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_exists_previous_split) + (ff_a_efrd_fubini_row_split_exists_previous_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_previous_split_successor_count_sum_partial. ff_h_efrd_fubini_row_split_exists_previous_split_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_exists_previous_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_previous_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_split_successor_count_sum_partial. ff_u_efrd_fubini_row_split_exists_previous_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_previous_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_exists_previous_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_split_successor_count_sum) + (ff_r_efrd_fubini_row_split_exists_previous_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_previous_split_successor_count_sum_successor. ff_h_efrd_fubini_row_split_exists_previous_split_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_exists_previous_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_exists_previous_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_split_successor_count_sum_successor. ff_u_efrd_fubini_row_split_exists_previous_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_previous_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_exists_previous_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_split_successor_count_sum) + (ff_s_efrd_fubini_row_split_exists_previous_split_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_exists_previous_split_successor_count_sum = ff_r_efrd_fubini_row_split_exists_previous_split_successor_count_sum + ff_a_efrd_fubini_row_split_exists_previous_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_exists_previous_split_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_exists_previous_split_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_exists_previous_split_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_exists_previous_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_exists_previous_split_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_exists_previous_split_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_exists_previous_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_exists_previous_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_exists_previous_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_exists_previous_split)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_split_successor_count_bits_decoded. efrd_row_code_fubini_row_split_exists_previous_split = ff_q_efrd_fubini_row_split_exists_previous_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_exists_previous_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_exists_previous_split) + (ff_bit_efrd_fubini_row_split_exists_previous_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_exists_previous_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_exists_previous_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_exists_previous_split_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_exists_previous_split_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_exists_previous_split_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_exists_previous_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_exists_previous_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_exists_previous_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_exists_previous_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_exists_previous_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_exists_previous_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_exists_previous_split)) /\ exists ff_q_eri_efrd_fubini_row_split_exists_previous_split_reduced_prefix_decoded. efrd_row_code_fubini_row_split_exists_previous_split = ff_q_eri_efrd_fubini_row_split_exists_previous_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_exists_previous_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_exists_previous_split) + (eri_bit_efrd_fubini_row_split_exists_previous_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_exists_previous_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_exists_previous_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_previous_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_previous) = p * S eri_column_efrd_fubini_row_split_exists_previous_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_previous_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_previous_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_previous_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_exists_previous))) \/ (eri_bit_efrd_fubini_row_split_exists_previous_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_exists_previous_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_previous_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_previous_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_exists_previous) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_previous_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_previous_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_previous) = p * S eri_column_efrd_fubini_row_split_exists_previous_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_exists_previous_split_terminal_entry. ff_h_efrd_fubini_row_split_exists_previous_split_terminal_entry + S (efrd_terminal_bit_fubini_row_split_exists_previous) = S ((S (h)) * efrd_row_scale_fubini_row_split_exists_previous_split)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_split_terminal_entry. efrd_row_code_fubini_row_split_exists_previous_split = ff_q_efrd_fubini_row_split_exists_previous_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_exists_previous_split) + (efrd_terminal_bit_fubini_row_split_exists_previous))))) /\ (((((exists ff_u_efrd_fubini_row_split_exists_previous_split_reduced_count_sum ff_v_efrd_fubini_row_split_exists_previous_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_start. ff_h_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_exists_previous_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_start. ff_u_efrd_fubini_row_split_exists_previous_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_exists_previous_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_row_split_exists_previous) = S ((S (h)) * ff_v_efrd_fubini_row_split_exists_previous_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_exists_previous_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_exists_previous_split_reduced_count_sum) + (efrd_reduced_count_fubini_row_split_exists_previous))) /\ forall ff_i_efrd_fubini_row_split_exists_previous_split_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_exists_previous_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_exists_previous_split_reduced_count_sum ff_r_efrd_fubini_row_split_exists_previous_split_reduced_count_sum ff_s_efrd_fubini_row_split_exists_previous_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_exists_previous_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_previous_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_exists_previous_split)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_summand. efrd_row_code_fubini_row_split_exists_previous_split = ff_q_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_exists_previous_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_exists_previous_split) + (ff_a_efrd_fubini_row_split_exists_previous_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_exists_previous_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_previous_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_exists_previous_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_exists_previous_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_split_reduced_count_sum) + (ff_r_efrd_fubini_row_split_exists_previous_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_exists_previous_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_exists_previous_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_exists_previous_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_previous_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_exists_previous_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_split_reduced_count_sum) + (ff_s_efrd_fubini_row_split_exists_previous_split_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_exists_previous_split_reduced_count_sum = ff_r_efrd_fubini_row_split_exists_previous_split_reduced_count_sum + ff_a_efrd_fubini_row_split_exists_previous_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_exists_previous_split_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_exists_previous_split_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_exists_previous_split_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_exists_previous_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_exists_previous_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_exists_previous_split_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_exists_previous_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_exists_previous_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_exists_previous_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_exists_previous_split)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_split_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_exists_previous_split = ff_q_efrd_fubini_row_split_exists_previous_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_exists_previous_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_exists_previous_split) + (ff_bit_efrd_fubini_row_split_exists_previous_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_exists_previous_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_exists_previous_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_row_split_exists_previous = 0 \/ efrd_terminal_bit_fubini_row_split_exists_previous = 1)) /\ efrd_count_fubini_row_split_exists_previous = efrd_reduced_count_fubini_row_split_exists_previous + efrd_terminal_bit_fubini_row_split_exists_previous)))))
27. 0027intro i
28. 0028intro hi
29. 0029specialize hchoices i
30. 0030apply hchoices
31. 0031specialize le_succ (S i)
32. 0032specialize le_succ l
33. 0033apply le_succ
34. 0034exact hi
35. 0035have hprevious_prefix : exists db dc tb tc. (forall efrd_row_index_fubini_row_split_exists_previous_prefix. (exists efrd_lt_gap_fubini_row_split_exists_previous_prefix_bound. efrd_lt_gap_fubini_row_split_exists_previous_prefix_bound + S (efrd_row_index_fubini_row_split_exists_previous_prefix) = l) -> exists efrd_count_fubini_row_split_exists_previous_prefix efrd_reduced_count_fubini_row_split_exists_previous_prefix efrd_terminal_bit_fubini_row_split_exists_previous_prefix. (((((((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_outer_entry. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_outer_entry + S (efrd_count_fubini_row_split_exists_previous_prefix) = S ((S (efrd_row_index_fubini_row_split_exists_previous_prefix)) * bc)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_outer_entry. bb = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_outer_entry * S ((S (efrd_row_index_fubini_row_split_exists_previous_prefix)) * bc) + (efrd_count_fubini_row_split_exists_previous_prefix))) /\ (((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_reduced_entry. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_reduced_entry + S (efrd_reduced_count_fubini_row_split_exists_previous_prefix) = S ((S (efrd_row_index_fubini_row_split_exists_previous_prefix)) * dc)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_reduced_entry. db = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_reduced_entry * S ((S (efrd_row_index_fubini_row_split_exists_previous_prefix)) * dc) + (efrd_reduced_count_fubini_row_split_exists_previous_prefix)))) /\ (((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_terminal_entry. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_terminal_entry + S (efrd_terminal_bit_fubini_row_split_exists_previous_prefix) = S ((S (efrd_row_index_fubini_row_split_exists_previous_prefix)) * tc)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_terminal_entry. tb = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_terminal_entry * S ((S (efrd_row_index_fubini_row_split_exists_previous_prefix)) * tc) + (efrd_terminal_bit_fubini_row_split_exists_previous_prefix)))) /\ (exists efrd_row_code_fubini_row_split_exists_previous_prefix_entry_split efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split. (((((forall eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix. (exists eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_bound. eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split)) /\ exists ff_q_eri_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_decoded. efrd_row_code_fubini_row_split_exists_previous_prefix_entry_split = ff_q_eri_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split) + (eri_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_previous_prefix) = p * S eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_exists_previous_prefix))) \/ (eri_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_exists_previous_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_previous_prefix) = p * S eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_start. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_start. ff_u_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_terminal + S (efrd_count_fubini_row_split_exists_previous_prefix) = S ((S (sh)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum) + (efrd_count_fubini_row_split_exists_previous_prefix))) /\ forall ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum ff_r_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum ff_s_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_summand. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_summand. efrd_row_code_fubini_row_split_exists_previous_prefix_entry_split = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split) + (ff_a_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_partial. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_partial. ff_u_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum) + (ff_r_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_successor. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_successor. ff_u_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum) + (ff_s_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum = ff_r_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum + ff_a_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits_decoded. efrd_row_code_fubini_row_split_exists_previous_prefix_entry_split = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split) + (ff_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split)) /\ exists ff_q_eri_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_decoded. efrd_row_code_fubini_row_split_exists_previous_prefix_entry_split = ff_q_eri_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split) + (eri_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_previous_prefix) = p * S eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_exists_previous_prefix))) \/ (eri_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_exists_previous_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_previous_prefix) = p * S eri_column_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_terminal_entry. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_terminal_entry + S (efrd_terminal_bit_fubini_row_split_exists_previous_prefix) = S ((S (h)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_terminal_entry. efrd_row_code_fubini_row_split_exists_previous_prefix_entry_split = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split) + (efrd_terminal_bit_fubini_row_split_exists_previous_prefix))))) /\ (((((exists ff_u_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_start. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_start. ff_u_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_row_split_exists_previous_prefix) = S ((S (h)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum) + (efrd_reduced_count_fubini_row_split_exists_previous_prefix))) /\ forall ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum ff_r_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum ff_s_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_summand. efrd_row_code_fubini_row_split_exists_previous_prefix_entry_split = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split) + (ff_a_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum) + (ff_r_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum) + (ff_s_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum = ff_r_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum + ff_a_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_exists_previous_prefix_entry_split = ff_q_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_exists_previous_prefix_entry_split) + (ff_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_exists_previous_prefix_entry_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_row_split_exists_previous_prefix = 0 \/ efrd_terminal_bit_fubini_row_split_exists_previous_prefix = 1)) /\ efrd_count_fubini_row_split_exists_previous_prefix = efrd_reduced_count_fubini_row_split_exists_previous_prefix + efrd_terminal_bit_fubini_row_split_exists_previous_prefix)))))))
36. 0036apply IH
37. 0037exact hprevious_choices
38. 0038cases hprevious_prefix
39. 0039cases hprevious_prefix_witness
40. 0040cases hprevious_prefix_witness_witness
41. 0041cases hprevious_prefix_witness_witness_witness
42. 0042have hlast : exists n r a. ((((exists ff_h_fubini_row_split_extend_last_source. ff_h_fubini_row_split_extend_last_source + S (n) = S ((S (l)) * bc)) /\ exists ff_q_fubini_row_split_extend_last_source. bb = ff_q_fubini_row_split_extend_last_source * S ((S (l)) * bc) + (n))) /\ (exists efrd_row_code_fubini_row_split_extend_last_witness efrd_row_scale_fubini_row_split_extend_last_witness. (((((forall eri_column_efrd_fubini_row_split_extend_last_witness_successor_prefix. (exists eri_gap_efrd_fubini_row_split_extend_last_witness_successor_prefix_bound. eri_gap_efrd_fubini_row_split_extend_last_witness_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_extend_last_witness_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_extend_last_witness_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_extend_last_witness_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_extend_last_witness_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_extend_last_witness_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_extend_last_witness_successor_prefix)) * efrd_row_scale_fubini_row_split_extend_last_witness)) /\ exists ff_q_eri_efrd_fubini_row_split_extend_last_witness_successor_prefix_decoded. efrd_row_code_fubini_row_split_extend_last_witness = ff_q_eri_efrd_fubini_row_split_extend_last_witness_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_extend_last_witness_successor_prefix)) * efrd_row_scale_fubini_row_split_extend_last_witness) + (eri_bit_efrd_fubini_row_split_extend_last_witness_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_extend_last_witness_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_extend_last_witness_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_extend_last_witness_successor_prefix_choice_left + S (q * S l) = p * S eri_column_efrd_fubini_row_split_extend_last_witness_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_extend_last_witness_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_extend_last_witness_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_extend_last_witness_successor_prefix) = q * S l))) \/ (eri_bit_efrd_fubini_row_split_extend_last_witness_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_extend_last_witness_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_extend_last_witness_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_extend_last_witness_successor_prefix) = q * S l) /\ ~(exists eri_gap_efrd_fubini_row_split_extend_last_witness_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_extend_last_witness_successor_prefix_choice_left + S (q * S l) = p * S eri_column_efrd_fubini_row_split_extend_last_witness_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_extend_last_witness_successor_count_sum ff_v_efrd_fubini_row_split_extend_last_witness_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_extend_last_witness_successor_count_sum_start. ff_h_efrd_fubini_row_split_extend_last_witness_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_extend_last_witness_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_extend_last_witness_successor_count_sum_start. ff_u_efrd_fubini_row_split_extend_last_witness_successor_count_sum = ff_q_efrd_fubini_row_split_extend_last_witness_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_extend_last_witness_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_extend_last_witness_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_extend_last_witness_successor_count_sum_terminal + S (n) = S ((S (sh)) * ff_v_efrd_fubini_row_split_extend_last_witness_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_extend_last_witness_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_extend_last_witness_successor_count_sum = ff_q_efrd_fubini_row_split_extend_last_witness_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_extend_last_witness_successor_count_sum) + (n))) /\ forall ff_i_efrd_fubini_row_split_extend_last_witness_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_extend_last_witness_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_extend_last_witness_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_extend_last_witness_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_extend_last_witness_successor_count_sum ff_r_efrd_fubini_row_split_extend_last_witness_successor_count_sum ff_s_efrd_fubini_row_split_extend_last_witness_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_extend_last_witness_successor_count_sum_summand. ff_h_efrd_fubini_row_split_extend_last_witness_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_extend_last_witness_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_extend_last_witness_successor_count_sum)) * efrd_row_scale_fubini_row_split_extend_last_witness)) /\ exists ff_q_efrd_fubini_row_split_extend_last_witness_successor_count_sum_summand. efrd_row_code_fubini_row_split_extend_last_witness = ff_q_efrd_fubini_row_split_extend_last_witness_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_extend_last_witness_successor_count_sum)) * efrd_row_scale_fubini_row_split_extend_last_witness) + (ff_a_efrd_fubini_row_split_extend_last_witness_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_extend_last_witness_successor_count_sum_partial. ff_h_efrd_fubini_row_split_extend_last_witness_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_extend_last_witness_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_extend_last_witness_successor_count_sum)) * ff_v_efrd_fubini_row_split_extend_last_witness_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_extend_last_witness_successor_count_sum_partial. ff_u_efrd_fubini_row_split_extend_last_witness_successor_count_sum = ff_q_efrd_fubini_row_split_extend_last_witness_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_extend_last_witness_successor_count_sum)) * ff_v_efrd_fubini_row_split_extend_last_witness_successor_count_sum) + (ff_r_efrd_fubini_row_split_extend_last_witness_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_extend_last_witness_successor_count_sum_successor. ff_h_efrd_fubini_row_split_extend_last_witness_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_extend_last_witness_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_extend_last_witness_successor_count_sum)) * ff_v_efrd_fubini_row_split_extend_last_witness_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_extend_last_witness_successor_count_sum_successor. ff_u_efrd_fubini_row_split_extend_last_witness_successor_count_sum = ff_q_efrd_fubini_row_split_extend_last_witness_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_extend_last_witness_successor_count_sum)) * ff_v_efrd_fubini_row_split_extend_last_witness_successor_count_sum) + (ff_s_efrd_fubini_row_split_extend_last_witness_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_extend_last_witness_successor_count_sum = ff_r_efrd_fubini_row_split_extend_last_witness_successor_count_sum + ff_a_efrd_fubini_row_split_extend_last_witness_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_extend_last_witness_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_extend_last_witness_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_extend_last_witness_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_extend_last_witness_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_extend_last_witness_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_extend_last_witness_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_extend_last_witness_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_extend_last_witness_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_extend_last_witness_successor_count_bits)) * efrd_row_scale_fubini_row_split_extend_last_witness)) /\ exists ff_q_efrd_fubini_row_split_extend_last_witness_successor_count_bits_decoded. efrd_row_code_fubini_row_split_extend_last_witness = ff_q_efrd_fubini_row_split_extend_last_witness_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_extend_last_witness_successor_count_bits)) * efrd_row_scale_fubini_row_split_extend_last_witness) + (ff_bit_efrd_fubini_row_split_extend_last_witness_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_extend_last_witness_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_extend_last_witness_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_extend_last_witness_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_extend_last_witness_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_extend_last_witness_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_extend_last_witness_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_extend_last_witness_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_extend_last_witness_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_extend_last_witness_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_extend_last_witness_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_extend_last_witness_reduced_prefix)) * efrd_row_scale_fubini_row_split_extend_last_witness)) /\ exists ff_q_eri_efrd_fubini_row_split_extend_last_witness_reduced_prefix_decoded. efrd_row_code_fubini_row_split_extend_last_witness = ff_q_eri_efrd_fubini_row_split_extend_last_witness_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_extend_last_witness_reduced_prefix)) * efrd_row_scale_fubini_row_split_extend_last_witness) + (eri_bit_efrd_fubini_row_split_extend_last_witness_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_extend_last_witness_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_extend_last_witness_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_extend_last_witness_reduced_prefix_choice_left + S (q * S l) = p * S eri_column_efrd_fubini_row_split_extend_last_witness_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_extend_last_witness_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_extend_last_witness_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_extend_last_witness_reduced_prefix) = q * S l))) \/ (eri_bit_efrd_fubini_row_split_extend_last_witness_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_extend_last_witness_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_extend_last_witness_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_extend_last_witness_reduced_prefix) = q * S l) /\ ~(exists eri_gap_efrd_fubini_row_split_extend_last_witness_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_extend_last_witness_reduced_prefix_choice_left + S (q * S l) = p * S eri_column_efrd_fubini_row_split_extend_last_witness_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_extend_last_witness_terminal_entry. ff_h_efrd_fubini_row_split_extend_last_witness_terminal_entry + S (a) = S ((S (h)) * efrd_row_scale_fubini_row_split_extend_last_witness)) /\ exists ff_q_efrd_fubini_row_split_extend_last_witness_terminal_entry. efrd_row_code_fubini_row_split_extend_last_witness = ff_q_efrd_fubini_row_split_extend_last_witness_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_extend_last_witness) + (a))))) /\ (((((exists ff_u_efrd_fubini_row_split_extend_last_witness_reduced_count_sum ff_v_efrd_fubini_row_split_extend_last_witness_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_start. ff_h_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_extend_last_witness_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_start. ff_u_efrd_fubini_row_split_extend_last_witness_reduced_count_sum = ff_q_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_extend_last_witness_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_terminal + S (r) = S ((S (h)) * ff_v_efrd_fubini_row_split_extend_last_witness_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_extend_last_witness_reduced_count_sum = ff_q_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_extend_last_witness_reduced_count_sum) + (r))) /\ forall ff_i_efrd_fubini_row_split_extend_last_witness_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_extend_last_witness_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_extend_last_witness_reduced_count_sum ff_r_efrd_fubini_row_split_extend_last_witness_reduced_count_sum ff_s_efrd_fubini_row_split_extend_last_witness_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_extend_last_witness_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_extend_last_witness_reduced_count_sum)) * efrd_row_scale_fubini_row_split_extend_last_witness)) /\ exists ff_q_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_summand. efrd_row_code_fubini_row_split_extend_last_witness = ff_q_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_extend_last_witness_reduced_count_sum)) * efrd_row_scale_fubini_row_split_extend_last_witness) + (ff_a_efrd_fubini_row_split_extend_last_witness_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_extend_last_witness_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_extend_last_witness_reduced_count_sum)) * ff_v_efrd_fubini_row_split_extend_last_witness_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_extend_last_witness_reduced_count_sum = ff_q_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_extend_last_witness_reduced_count_sum)) * ff_v_efrd_fubini_row_split_extend_last_witness_reduced_count_sum) + (ff_r_efrd_fubini_row_split_extend_last_witness_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_extend_last_witness_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_extend_last_witness_reduced_count_sum)) * ff_v_efrd_fubini_row_split_extend_last_witness_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_extend_last_witness_reduced_count_sum = ff_q_efrd_fubini_row_split_extend_last_witness_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_extend_last_witness_reduced_count_sum)) * ff_v_efrd_fubini_row_split_extend_last_witness_reduced_count_sum) + (ff_s_efrd_fubini_row_split_extend_last_witness_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_extend_last_witness_reduced_count_sum = ff_r_efrd_fubini_row_split_extend_last_witness_reduced_count_sum + ff_a_efrd_fubini_row_split_extend_last_witness_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_extend_last_witness_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_extend_last_witness_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_extend_last_witness_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_extend_last_witness_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_extend_last_witness_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_extend_last_witness_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_extend_last_witness_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_extend_last_witness_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_extend_last_witness_reduced_count_bits)) * efrd_row_scale_fubini_row_split_extend_last_witness)) /\ exists ff_q_efrd_fubini_row_split_extend_last_witness_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_extend_last_witness = ff_q_efrd_fubini_row_split_extend_last_witness_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_extend_last_witness_reduced_count_bits)) * efrd_row_scale_fubini_row_split_extend_last_witness) + (ff_bit_efrd_fubini_row_split_extend_last_witness_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_extend_last_witness_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_extend_last_witness_reduced_count_bits = 1))))) /\ (a = 0 \/ a = 1)) /\ n = r + a)))))
43. 0043specialize hchoices l
44. 0044apply hchoices
45. 0045specialize le_refl (S l)
46. 0046exact le_refl
47. 0047have hnext : exists db dc tb tc. (forall efrd_row_index_fubini_row_split_exists_successor_prefix. (exists efrd_lt_gap_fubini_row_split_exists_successor_prefix_bound. efrd_lt_gap_fubini_row_split_exists_successor_prefix_bound + S (efrd_row_index_fubini_row_split_exists_successor_prefix) = S l) -> exists efrd_count_fubini_row_split_exists_successor_prefix efrd_reduced_count_fubini_row_split_exists_successor_prefix efrd_terminal_bit_fubini_row_split_exists_successor_prefix. (((((((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_outer_entry. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_outer_entry + S (efrd_count_fubini_row_split_exists_successor_prefix) = S ((S (efrd_row_index_fubini_row_split_exists_successor_prefix)) * bc)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_outer_entry. bb = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_outer_entry * S ((S (efrd_row_index_fubini_row_split_exists_successor_prefix)) * bc) + (efrd_count_fubini_row_split_exists_successor_prefix))) /\ (((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_reduced_entry. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_reduced_entry + S (efrd_reduced_count_fubini_row_split_exists_successor_prefix) = S ((S (efrd_row_index_fubini_row_split_exists_successor_prefix)) * dc)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_reduced_entry. db = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_reduced_entry * S ((S (efrd_row_index_fubini_row_split_exists_successor_prefix)) * dc) + (efrd_reduced_count_fubini_row_split_exists_successor_prefix)))) /\ (((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_terminal_entry. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_terminal_entry + S (efrd_terminal_bit_fubini_row_split_exists_successor_prefix) = S ((S (efrd_row_index_fubini_row_split_exists_successor_prefix)) * tc)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_terminal_entry. tb = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_terminal_entry * S ((S (efrd_row_index_fubini_row_split_exists_successor_prefix)) * tc) + (efrd_terminal_bit_fubini_row_split_exists_successor_prefix)))) /\ (exists efrd_row_code_fubini_row_split_exists_successor_prefix_entry_split efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split. (((((forall eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix. (exists eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_bound. eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split)) /\ exists ff_q_eri_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_decoded. efrd_row_code_fubini_row_split_exists_successor_prefix_entry_split = ff_q_eri_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split) + (eri_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_successor_prefix) = p * S eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_exists_successor_prefix))) \/ (eri_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_exists_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_successor_prefix) = p * S eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_start. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_start. ff_u_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_terminal + S (efrd_count_fubini_row_split_exists_successor_prefix) = S ((S (sh)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum) + (efrd_count_fubini_row_split_exists_successor_prefix))) /\ forall ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum ff_r_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum ff_s_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_summand. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_summand. efrd_row_code_fubini_row_split_exists_successor_prefix_entry_split = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split) + (ff_a_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_partial. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_partial. ff_u_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum) + (ff_r_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_successor. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_successor. ff_u_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum) + (ff_s_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum = ff_r_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum + ff_a_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits_decoded. efrd_row_code_fubini_row_split_exists_successor_prefix_entry_split = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split) + (ff_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split)) /\ exists ff_q_eri_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_decoded. efrd_row_code_fubini_row_split_exists_successor_prefix_entry_split = ff_q_eri_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split) + (eri_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_successor_prefix) = p * S eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_exists_successor_prefix))) \/ (eri_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_exists_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_successor_prefix) = p * S eri_column_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_terminal_entry. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_terminal_entry + S (efrd_terminal_bit_fubini_row_split_exists_successor_prefix) = S ((S (h)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_terminal_entry. efrd_row_code_fubini_row_split_exists_successor_prefix_entry_split = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split) + (efrd_terminal_bit_fubini_row_split_exists_successor_prefix))))) /\ (((((exists ff_u_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_start. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_start. ff_u_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_row_split_exists_successor_prefix) = S ((S (h)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum) + (efrd_reduced_count_fubini_row_split_exists_successor_prefix))) /\ forall ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum ff_r_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum ff_s_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_summand. efrd_row_code_fubini_row_split_exists_successor_prefix_entry_split = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split) + (ff_a_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum) + (ff_r_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum) + (ff_s_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum = ff_r_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum + ff_a_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_exists_successor_prefix_entry_split = ff_q_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_exists_successor_prefix_entry_split) + (ff_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_exists_successor_prefix_entry_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_row_split_exists_successor_prefix = 0 \/ efrd_terminal_bit_fubini_row_split_exists_successor_prefix = 1)) /\ efrd_count_fubini_row_split_exists_successor_prefix = efrd_reduced_count_fubini_row_split_exists_successor_prefix + efrd_terminal_bit_fubini_row_split_exists_successor_prefix)))))))
48. 0048specialize eisenstein_successor_row_split_prefix_extend p
49. 0049specialize eisenstein_successor_row_split_prefix_extend q
50. 0050specialize eisenstein_successor_row_split_prefix_extend h
51. 0051specialize eisenstein_successor_row_split_prefix_extend sh
52. 0052specialize eisenstein_successor_row_split_prefix_extend bb
53. 0053specialize eisenstein_successor_row_split_prefix_extend bc
54. 0054specialize eisenstein_successor_row_split_prefix_extend x
55. 0055specialize eisenstein_successor_row_split_prefix_extend x1
56. 0056specialize eisenstein_successor_row_split_prefix_extend x2
57. 0057specialize eisenstein_successor_row_split_prefix_extend x3
58. 0058specialize eisenstein_successor_row_split_prefix_extend l
59. 0059apply eisenstein_successor_row_split_prefix_extend
60. 0060exact hprevious_prefix_witness_witness_witness_witness
61. 0061exact hlast
62. 0062exact hnext