Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Statement with defined notation
∀ p. ∀ q. ∀ h. ∀ sh. ∀ bb. ∀ bc. ∀ l. (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(bb,bc,x,y) ∧ (∃ m. ∃ k. (∀ i. Lt(i,sh) → ∃ j. BetaAt(m,k,i,j) ∧ (j = 0 ∧ (Lt(q · S x,p · S i) ∧ ¬Lt(p · S i,q · S x)) ∨ j = 1 ∧ (Lt(p · S i,q · S x) ∧ ¬Lt(q · S x,p · S i)))) ∧ BitCount(m,k,sh,y) ∧ ((∀ i. Lt(i,h) → ∃ j. BetaAt(m,k,i,j) ∧ (j = 0 ∧ (Lt(q · S x,p · S i) ∧ ¬Lt(p · S i,q · S x)) ∨ j = 1 ∧ (Lt(p · S i,q · S x) ∧ ¬Lt(q · S x,p · S i)))) ∧ BetaAt(m,k,h,n)) ∧ (BitCount(m,k,h,z) ∧ (n = 0 ∨ n = 1) ∧ y = z + n))) → ∃ x. ∃ y. ∃ z. ∃ n. ∀ m. Lt(m,l) → ∃ k. ∃ i. ∃ j. BetaAt(bb,bc,m,k) ∧ BetaAt(x,y,m,i) ∧ BetaAt(z,n,m,j) ∧ (∃ u. ∃ v. (∀ w. Lt(w,sh) → ∃ x0. BetaAt(u,v,w,x0) ∧ (x0 = 0 ∧ (Lt(q · S m,p · S w) ∧ ¬Lt(p · S w,q · S m)) ∨ x0 = 1 ∧ (Lt(p · S w,q · S m) ∧ ¬Lt(q · S m,p · S w)))) ∧ BitCount(u,v,sh,k) ∧ ((∀ w. Lt(w,h) → ∃ x0. BetaAt(u,v,w,x0) ∧ (x0 = 0 ∧ (Lt(q · S m,p · S w) ∧ ¬Lt(p · S w,q · S m)) ∨ x0 = 1 ∧ (Lt(p · S w,q · S m) ∧ ¬Lt(q · S m,p · S w)))) ∧ BetaAt(u,v,h,j)) ∧ (BitCount(u,v,h,i) ∧ (j = 0 ∨ j = 1) ∧ k = i + j))Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.
Definitions used by this theorem
In the theorem statement
36 occurrences
In local proof propositions
71 occurrences
Exact expanded native-PA statement
forall p q h sh bb bc l. (forall efrd_row_index_fubini_row_split_exists_all. (exists efrd_lt_gap_fubini_row_split_exists_all_bound. efrd_lt_gap_fubini_row_split_exists_all_bound + S (efrd_row_index_fubini_row_split_exists_all) = l) -> exists efrd_count_fubini_row_split_exists_all efrd_reduced_count_fubini_row_split_exists_all efrd_terminal_bit_fubini_row_split_exists_all. ((((exists ff_h_efrd_fubini_row_split_exists_all_outer_entry. ff_h_efrd_fubini_row_split_exists_all_outer_entry + S (efrd_count_fubini_row_split_exists_all) = S ((S (efrd_row_index_fubini_row_split_exists_all)) * bc)) /\ exists ff_q_efrd_fubini_row_split_exists_all_outer_entry. bb = ff_q_efrd_fubini_row_split_exists_all_outer_entry * S ((S (efrd_row_index_fubini_row_split_exists_all)) * bc) + (efrd_count_fubini_row_split_exists_all))) /\ (exists efrd_row_code_fubini_row_split_exists_all_split efrd_row_scale_fubini_row_split_exists_all_split. (((((forall eri_column_efrd_fubini_row_split_exists_all_split_successor_prefix. (exists eri_gap_efrd_fubini_row_split_exists_all_split_successor_prefix_bound. eri_gap_efrd_fubini_row_split_exists_all_split_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_exists_all_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_exists_all_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_exists_all_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_exists_all_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_exists_all_split_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_exists_all_split_successor_prefix)) * efrd_row_scale_fubini_row_split_exists_all_split)) /\ exists ff_q_eri_efrd_fubini_row_split_exists_all_split_successor_prefix_decoded. efrd_row_code_fubini_row_split_exists_all_split = ff_q_eri_efrd_fubini_row_split_exists_all_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_exists_all_split_successor_prefix)) * efrd_row_scale_fubini_row_split_exists_all_split) + (eri_bit_efrd_fubini_row_split_exists_all_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_exists_all_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_exists_all_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_all_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_all) = p * S eri_column_efrd_fubini_row_split_exists_all_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_all_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_all_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_all_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_exists_all))) \/ (eri_bit_efrd_fubini_row_split_exists_all_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_exists_all_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_all_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_all_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_exists_all) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_all_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_all_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_all) = p * S eri_column_efrd_fubini_row_split_exists_all_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_exists_all_split_successor_count_sum ff_v_efrd_fubini_row_split_exists_all_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_all_split_successor_count_sum_start. ff_h_efrd_fubini_row_split_exists_all_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_exists_all_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_all_split_successor_count_sum_start. ff_u_efrd_fubini_row_split_exists_all_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_all_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_exists_all_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_all_split_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_exists_all_split_successor_count_sum_terminal + S (efrd_count_fubini_row_split_exists_all) = S ((S (sh)) * ff_v_efrd_fubini_row_split_exists_all_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_all_split_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_exists_all_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_all_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_exists_all_split_successor_count_sum) + (efrd_count_fubini_row_split_exists_all))) /\ forall ff_i_efrd_fubini_row_split_exists_all_split_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_exists_all_split_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_exists_all_split_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_exists_all_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_exists_all_split_successor_count_sum ff_r_efrd_fubini_row_split_exists_all_split_successor_count_sum ff_s_efrd_fubini_row_split_exists_all_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_all_split_successor_count_sum_summand. ff_h_efrd_fubini_row_split_exists_all_split_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_exists_all_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_all_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_exists_all_split)) /\ exists ff_q_efrd_fubini_row_split_exists_all_split_successor_count_sum_summand. efrd_row_code_fubini_row_split_exists_all_split = ff_q_efrd_fubini_row_split_exists_all_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_exists_all_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_exists_all_split) + (ff_a_efrd_fubini_row_split_exists_all_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_all_split_successor_count_sum_partial. ff_h_efrd_fubini_row_split_exists_all_split_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_exists_all_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_all_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_all_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_all_split_successor_count_sum_partial. ff_u_efrd_fubini_row_split_exists_all_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_all_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_exists_all_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_all_split_successor_count_sum) + (ff_r_efrd_fubini_row_split_exists_all_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_all_split_successor_count_sum_successor. ff_h_efrd_fubini_row_split_exists_all_split_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_exists_all_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_exists_all_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_all_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_all_split_successor_count_sum_successor. ff_u_efrd_fubini_row_split_exists_all_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_all_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_exists_all_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_all_split_successor_count_sum) + (ff_s_efrd_fubini_row_split_exists_all_split_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_exists_all_split_successor_count_sum = ff_r_efrd_fubini_row_split_exists_all_split_successor_count_sum + ff_a_efrd_fubini_row_split_exists_all_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_exists_all_split_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_exists_all_split_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_exists_all_split_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_exists_all_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_exists_all_split_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_exists_all_split_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_exists_all_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_exists_all_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_exists_all_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_exists_all_split)) /\ exists ff_q_efrd_fubini_row_split_exists_all_split_successor_count_bits_decoded. efrd_row_code_fubini_row_split_exists_all_split = ff_q_efrd_fubini_row_split_exists_all_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_exists_all_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_exists_all_split) + (ff_bit_efrd_fubini_row_split_exists_all_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_exists_all_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_exists_all_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_exists_all_split_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_exists_all_split_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_exists_all_split_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_exists_all_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_exists_all_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_exists_all_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_exists_all_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_exists_all_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_exists_all_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_exists_all_split)) /\ exists ff_q_eri_efrd_fubini_row_split_exists_all_split_reduced_prefix_decoded. efrd_row_code_fubini_row_split_exists_all_split = ff_q_eri_efrd_fubini_row_split_exists_all_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_exists_all_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_exists_all_split) + (eri_bit_efrd_fubini_row_split_exists_all_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_exists_all_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_exists_all_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_all_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_all) = p * S eri_column_efrd_fubini_row_split_exists_all_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_all_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_all_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_all_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_exists_all))) \/ (eri_bit_efrd_fubini_row_split_exists_all_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_exists_all_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_all_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_all_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_exists_all) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_all_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_all_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_all) = p * S eri_column_efrd_fubini_row_split_exists_all_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_exists_all_split_terminal_entry. ff_h_efrd_fubini_row_split_exists_all_split_terminal_entry + S (efrd_terminal_bit_fubini_row_split_exists_all) = S ((S (h)) * efrd_row_scale_fubini_row_split_exists_all_split)) /\ exists ff_q_efrd_fubini_row_split_exists_all_split_terminal_entry. efrd_row_code_fubini_row_split_exists_all_split = ff_q_efrd_fubini_row_split_exists_all_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_exists_all_split) + (efrd_terminal_bit_fubini_row_split_exists_all))))) /\ (((((exists ff_u_efrd_fubini_row_split_exists_all_split_reduced_count_sum ff_v_efrd_fubini_row_split_exists_all_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_all_split_reduced_count_sum_start. ff_h_efrd_fubini_row_split_exists_all_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_exists_all_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_all_split_reduced_count_sum_start. ff_u_efrd_fubini_row_split_exists_all_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_all_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_exists_all_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_all_split_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_exists_all_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_row_split_exists_all) = S ((S (h)) * ff_v_efrd_fubini_row_split_exists_all_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_all_split_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_exists_all_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_all_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_exists_all_split_reduced_count_sum) + (efrd_reduced_count_fubini_row_split_exists_all))) /\ forall ff_i_efrd_fubini_row_split_exists_all_split_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_exists_all_split_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_exists_all_split_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_exists_all_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_exists_all_split_reduced_count_sum ff_r_efrd_fubini_row_split_exists_all_split_reduced_count_sum ff_s_efrd_fubini_row_split_exists_all_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_all_split_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_exists_all_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_exists_all_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_all_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_exists_all_split)) /\ exists ff_q_efrd_fubini_row_split_exists_all_split_reduced_count_sum_summand. efrd_row_code_fubini_row_split_exists_all_split = ff_q_efrd_fubini_row_split_exists_all_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_exists_all_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_exists_all_split) + (ff_a_efrd_fubini_row_split_exists_all_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_all_split_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_exists_all_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_exists_all_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_all_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_all_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_all_split_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_exists_all_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_all_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_exists_all_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_all_split_reduced_count_sum) + (ff_r_efrd_fubini_row_split_exists_all_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_all_split_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_exists_all_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_exists_all_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_exists_all_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_all_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_all_split_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_exists_all_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_all_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_exists_all_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_all_split_reduced_count_sum) + (ff_s_efrd_fubini_row_split_exists_all_split_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_exists_all_split_reduced_count_sum = ff_r_efrd_fubini_row_split_exists_all_split_reduced_count_sum + ff_a_efrd_fubini_row_split_exists_all_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_exists_all_split_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_exists_all_split_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_exists_all_split_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_exists_all_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_exists_all_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_exists_all_split_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_exists_all_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_exists_all_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_exists_all_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_exists_all_split)) /\ exists ff_q_efrd_fubini_row_split_exists_all_split_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_exists_all_split = ff_q_efrd_fubini_row_split_exists_all_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_exists_all_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_exists_all_split) + (ff_bit_efrd_fubini_row_split_exists_all_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_exists_all_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_exists_all_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_row_split_exists_all = 0 \/ efrd_terminal_bit_fubini_row_split_exists_all = 1)) /\ efrd_count_fubini_row_split_exists_all = efrd_reduced_count_fubini_row_split_exists_all + efrd_terminal_bit_fubini_row_split_exists_all)))))) -> (exists db dc tb tc. (forall efrd_row_index_fubini_row_split_exists_result. (exists efrd_lt_gap_fubini_row_split_exists_result_bound. efrd_lt_gap_fubini_row_split_exists_result_bound + S (efrd_row_index_fubini_row_split_exists_result) = l) -> exists efrd_count_fubini_row_split_exists_result efrd_reduced_count_fubini_row_split_exists_result efrd_terminal_bit_fubini_row_split_exists_result. (((((((exists ff_h_efrd_fubini_row_split_exists_result_entry_outer_entry. ff_h_efrd_fubini_row_split_exists_result_entry_outer_entry + S (efrd_count_fubini_row_split_exists_result) = S ((S (efrd_row_index_fubini_row_split_exists_result)) * bc)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_outer_entry. bb = ff_q_efrd_fubini_row_split_exists_result_entry_outer_entry * S ((S (efrd_row_index_fubini_row_split_exists_result)) * bc) + (efrd_count_fubini_row_split_exists_result))) /\ (((exists ff_h_efrd_fubini_row_split_exists_result_entry_reduced_entry. ff_h_efrd_fubini_row_split_exists_result_entry_reduced_entry + S (efrd_reduced_count_fubini_row_split_exists_result) = S ((S (efrd_row_index_fubini_row_split_exists_result)) * dc)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_reduced_entry. db = ff_q_efrd_fubini_row_split_exists_result_entry_reduced_entry * S ((S (efrd_row_index_fubini_row_split_exists_result)) * dc) + (efrd_reduced_count_fubini_row_split_exists_result)))) /\ (((exists ff_h_efrd_fubini_row_split_exists_result_entry_terminal_entry. ff_h_efrd_fubini_row_split_exists_result_entry_terminal_entry + S (efrd_terminal_bit_fubini_row_split_exists_result) = S ((S (efrd_row_index_fubini_row_split_exists_result)) * tc)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_terminal_entry. tb = ff_q_efrd_fubini_row_split_exists_result_entry_terminal_entry * S ((S (efrd_row_index_fubini_row_split_exists_result)) * tc) + (efrd_terminal_bit_fubini_row_split_exists_result)))) /\ (exists efrd_row_code_fubini_row_split_exists_result_entry_split efrd_row_scale_fubini_row_split_exists_result_entry_split. (((((forall eri_column_efrd_fubini_row_split_exists_result_entry_split_successor_prefix. (exists eri_gap_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_bound. eri_gap_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_exists_result_entry_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_exists_result_entry_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_exists_result_entry_split_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_exists_result_entry_split_successor_prefix)) * efrd_row_scale_fubini_row_split_exists_result_entry_split)) /\ exists ff_q_eri_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_decoded. efrd_row_code_fubini_row_split_exists_result_entry_split = ff_q_eri_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_exists_result_entry_split_successor_prefix)) * efrd_row_scale_fubini_row_split_exists_result_entry_split) + (eri_bit_efrd_fubini_row_split_exists_result_entry_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_exists_result_entry_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_result) = p * S eri_column_efrd_fubini_row_split_exists_result_entry_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_result_entry_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_exists_result))) \/ (eri_bit_efrd_fubini_row_split_exists_result_entry_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_result_entry_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_exists_result) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_result_entry_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_result) = p * S eri_column_efrd_fubini_row_split_exists_result_entry_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum ff_v_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_start. ff_h_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_start. ff_u_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_terminal + S (efrd_count_fubini_row_split_exists_result) = S ((S (sh)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum) + (efrd_count_fubini_row_split_exists_result))) /\ forall ff_i_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum ff_r_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum ff_s_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_summand. ff_h_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_exists_result_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_summand. efrd_row_code_fubini_row_split_exists_result_entry_split = ff_q_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_exists_result_entry_split) + (ff_a_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_partial. ff_h_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_partial. ff_u_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum) + (ff_r_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_successor. ff_h_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_successor. ff_u_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum) + (ff_s_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum = ff_r_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum + ff_a_efrd_fubini_row_split_exists_result_entry_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_exists_result_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits_decoded. efrd_row_code_fubini_row_split_exists_result_entry_split = ff_q_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_exists_result_entry_split) + (ff_bit_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_exists_result_entry_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_exists_result_entry_split)) /\ exists ff_q_eri_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_decoded. efrd_row_code_fubini_row_split_exists_result_entry_split = ff_q_eri_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_exists_result_entry_split) + (eri_bit_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_result) = p * S eri_column_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_exists_result))) \/ (eri_bit_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_exists_result) /\ ~(exists eri_gap_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_exists_result) = p * S eri_column_efrd_fubini_row_split_exists_result_entry_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_exists_result_entry_split_terminal_entry. ff_h_efrd_fubini_row_split_exists_result_entry_split_terminal_entry + S (efrd_terminal_bit_fubini_row_split_exists_result) = S ((S (h)) * efrd_row_scale_fubini_row_split_exists_result_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_split_terminal_entry. efrd_row_code_fubini_row_split_exists_result_entry_split = ff_q_efrd_fubini_row_split_exists_result_entry_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_exists_result_entry_split) + (efrd_terminal_bit_fubini_row_split_exists_result))))) /\ (((((exists ff_u_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum ff_v_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_start. ff_h_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_start. ff_u_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_row_split_exists_result) = S ((S (h)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum) + (efrd_reduced_count_fubini_row_split_exists_result))) /\ forall ff_i_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum ff_r_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum ff_s_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_exists_result_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_summand. efrd_row_code_fubini_row_split_exists_result_entry_split = ff_q_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_exists_result_entry_split) + (ff_a_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum) + (ff_r_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum) + (ff_s_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum = ff_r_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum + ff_a_efrd_fubini_row_split_exists_result_entry_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_exists_result_entry_split)) /\ exists ff_q_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_exists_result_entry_split = ff_q_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_exists_result_entry_split) + (ff_bit_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_exists_result_entry_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_row_split_exists_result = 0 \/ efrd_terminal_bit_fubini_row_split_exists_result = 1)) /\ efrd_count_fubini_row_split_exists_result = efrd_reduced_count_fubini_row_split_exists_result + efrd_terminal_bit_fubini_row_split_exists_result))))))))Proof neighborhood
Direct theorem prerequisites
PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA00EW eisenstein_successor_row_split_prefix_extendDirect theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (5)
01Fix variables and assumptionsL1–6
02Induction on lL7–8
03Construct an explicit witnessL9–12
04Fix variables and assumptionsL13–14
05Separate the logical casesL15–16
06Establish hsiL17–25
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.
07Establish hprevious_choicesL26–34
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hchoices.
- L26Definitions: Lt(efrd_row_index_fubini_row_split_exists_previous,l)BetaAt(bb,bc,efrd_row_index_fubini_row_split_exists_previous,x)Lt(k,sh)BetaAt(n,m,k,i)Lt(q · S efrd_row_index_fubini_row_split_exists_previous,p · S k)Lt(p · S k,q · S efrd_row_index_fubini_row_split_exists_previous)BitCount(n,m,sh,x)Lt(k,h)BetaAt(n,m,h,z)BitCount(n,m,h,y)Original native command in the exact edition
have hprevious_choices · expand full local formula (988 characters)
have hprevious_choices : ∀ efrd_row_index_fubini_row_split_exists_previous. Lt(efrd_row_index_fubini_row_split_exists_previous,l) → ∃ x. ∃ y. ∃ z. BetaAt(bb,bc,efrd_row_index_fubini_row_split_exists_previous,x) ∧ (∃ n. ∃ m. (∀ k. Lt(k,sh) → ∃ i. BetaAt(n,m,k,i) ∧ (i = 0 ∧ (Lt(q · S efrd_row_index_fubini_row_split_exists_previous,p · S k) ∧ ¬Lt(p · S k,q · S efrd_row_index_fubini_row_split_exists_previous)) ∨ i = 1 ∧ (Lt(p · S k,q · S efrd_row_index_fubini_row_split_exists_previous) ∧ ¬Lt(q · S efrd_row_index_fubini_row_split_exists_previous,p · S k)))) ∧ BitCount(n,m,sh,x) ∧ ((∀ k. Lt(k,h) → ∃ i. BetaAt(n,m,k,i) ∧ (i = 0 ∧ (Lt(q · S efrd_row_index_fubini_row_split_exists_previous,p · S k) ∧ ¬Lt(p · S k,q · S efrd_row_index_fubini_row_split_exists_previous)) ∨ i = 1 ∧ (Lt(p · S k,q · S efrd_row_index_fubini_row_split_exists_previous) ∧ ¬Lt(q · S efrd_row_index_fubini_row_split_exists_previous,p · S k)))) ∧ BetaAt(n,m,h,z)) ∧ (BitCount(n,m,h,y) ∧ (z = 0 ∨ z = 1) ∧ x = y + z)) - L27
intro i - L28
intro hi - L29
specialize hchoices i - L30
apply hchoices - L31
specialize le_succ (S i) - L32
specialize le_succ l - L33
apply le_succ - L34
exact hi
08Establish hprevious_prefixL35–37
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
- L35
have hprevious_prefix : ∃ db. ∃ dc. ∃ tb. ∃ tc. ∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(bb,bc,x,y) ∧ BetaAt(db,dc,x,z) ∧ BetaAt(tb,tc,x,n) ∧ (∃ m. ∃ k. (∀ i. Lt(i,sh) → ∃ j. BetaAt(m,k,i,j) ∧ (j = 0 ∧ (Lt(q · S x,p · S i) ∧ ¬Lt(p · S i,q · S x)) ∨ j = 1 ∧ (Lt(p · S i,q · S x) ∧ ¬Lt(q · S x,p · S i)))) ∧ BitCount(m,k,sh,y) ∧ ((∀ i. Lt(i,h) → ∃ j. BetaAt(m,k,i,j) ∧ (j = 0 ∧ (Lt(q · S x,p · S i) ∧ ¬Lt(p · S i,q · S x)) ∨ j = 1 ∧ (Lt(p · S i,q · S x) ∧ ¬Lt(q · S x,p · S i)))) ∧ BetaAt(m,k,h,n)) ∧ (BitCount(m,k,h,z) ∧ (n = 0 ∨ n = 1) ∧ y = z + n))Definitions: Lt(x,l)BetaAt(bb,bc,x,y)BetaAt(db,dc,x,z)BetaAt(tb,tc,x,n)Lt(i,sh)BetaAt(m,k,i,j)Lt(q · S x,p · S i)Lt(p · S i,q · S x)BitCount(m,k,sh,y)Lt(i,h)BetaAt(m,k,h,n)BitCount(m,k,h,z)Original native command in the exact edition - L36
apply IH - L37
exact hprevious_choices
09Separate the logical casesL38–41
10Establish hlastL42–46
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hchoices.
- L42
have hlast : ∃ n. ∃ r. ∃ a. BetaAt(bb,bc,l,n) ∧ (∃ x. ∃ y. (∀ z. Lt(z,sh) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(q · S l,p · S z) ∧ ¬Lt(p · S z,q · S l)) ∨ m = 1 ∧ (Lt(p · S z,q · S l) ∧ ¬Lt(q · S l,p · S z)))) ∧ BitCount(x,y,sh,n) ∧ ((∀ z. Lt(z,h) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(q · S l,p · S z) ∧ ¬Lt(p · S z,q · S l)) ∨ m = 1 ∧ (Lt(p · S z,q · S l) ∧ ¬Lt(q · S l,p · S z)))) ∧ BetaAt(x,y,h,a)) ∧ (BitCount(x,y,h,r) ∧ (a = 0 ∨ a = 1) ∧ n = r + a))Definitions: BetaAt(bb,bc,l,n)Lt(z,sh)BetaAt(x,y,z,m)Lt(q · S l,p · S z)Lt(p · S z,q · S l)BitCount(x,y,sh,n)Lt(z,h)BetaAt(x,y,h,a)BitCount(x,y,h,r)Original native command in the exact edition - L43
specialize hchoices l - L44
apply hchoices - L45
specialize le_refl (S l) - L46
exact le_refl
11Establish hnextL47–56
Establish this local claim before using it. It is not an additional assumption.
- L47
have hnext : ∃ db. ∃ dc. ∃ tb. ∃ tc. ∀ x. Lt(x,S l) → ∃ y. ∃ z. ∃ n. BetaAt(bb,bc,x,y) ∧ BetaAt(db,dc,x,z) ∧ BetaAt(tb,tc,x,n) ∧ (∃ m. ∃ k. (∀ i. Lt(i,sh) → ∃ j. BetaAt(m,k,i,j) ∧ (j = 0 ∧ (Lt(q · S x,p · S i) ∧ ¬Lt(p · S i,q · S x)) ∨ j = 1 ∧ (Lt(p · S i,q · S x) ∧ ¬Lt(q · S x,p · S i)))) ∧ BitCount(m,k,sh,y) ∧ ((∀ i. Lt(i,h) → ∃ j. BetaAt(m,k,i,j) ∧ (j = 0 ∧ (Lt(q · S x,p · S i) ∧ ¬Lt(p · S i,q · S x)) ∨ j = 1 ∧ (Lt(p · S i,q · S x) ∧ ¬Lt(q · S x,p · S i)))) ∧ BetaAt(m,k,h,n)) ∧ (BitCount(m,k,h,z) ∧ (n = 0 ∨ n = 1) ∧ y = z + n))Definitions: Lt(x,S l)BetaAt(bb,bc,x,y)BetaAt(db,dc,x,z)BetaAt(tb,tc,x,n)Lt(i,sh)BetaAt(m,k,i,j)Lt(q · S x,p · S i)Lt(p · S i,q · S x)BitCount(m,k,sh,y)Lt(i,h)BetaAt(m,k,h,n)BitCount(m,k,h,z)Original native command in the exact edition - L48
specialize eisenstein_successor_row_split_prefix_extend p - L49
specialize eisenstein_successor_row_split_prefix_extend q - L50
specialize eisenstein_successor_row_split_prefix_extend h - L51
specialize eisenstein_successor_row_split_prefix_extend sh - L52
specialize eisenstein_successor_row_split_prefix_extend bb - L53
specialize eisenstein_successor_row_split_prefix_extend bc - L54
specialize eisenstein_successor_row_split_prefix_extend x - L55
specialize eisenstein_successor_row_split_prefix_extend x1 - L56
specialize eisenstein_successor_row_split_prefix_extend x2
12Use earlier factsL57–62
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 62 lines
- 0001
intro p - 0002
intro q - 0003
intro h - 0004
intro sh - 0005
intro bb - 0006
intro bc - 0007
induction l - 0008
intro hchoices - 0009
exists 0 - 0010
exists 0 - 0011
exists 0 - 0012
exists 0 - 0013
intro i - 0014
intro hi - 0015
exfalso - 0016
cases hi - 0017
have hsi : S i = 0 - 0018
specialize add_eq_zero_right x - 0019
specialize add_eq_zero_right (S i) - 0020
apply add_eq_zero_right - 0021
exact hi_witness - 0022
specialize succ_ne_zero i - 0023
apply succ_ne_zero - 0024
exact hsi - 0025
intro hchoices - 0026
have hprevious_choices : ∀ efrd_row_index_fubini_row_split_exists_previous. Lt(efrd_row_index_fubini_row_split_exists_previous,l) → ∃ x. ∃ y. ∃ z. BetaAt(bb,bc,efrd_row_index_fubini_row_split_exists_previous,x) ∧ (∃ n. ∃ m. (∀ k. Lt(k,sh) → ∃ i. BetaAt(n,m,k,i) ∧ (i = 0 ∧ (Lt(q · S efrd_row_index_fubini_row_split_exists_previous,p · S k) ∧ ¬Lt(p · S k,q · S efrd_row_index_fubini_row_split_exists_previous)) ∨ i = 1 ∧ (Lt(p · S k,q · S efrd_row_index_fubini_row_split_exists_previous) ∧ ¬Lt(q · S efrd_row_index_fubini_row_split_exists_previous,p · S k)))) ∧ BitCount(n,m,sh,x) ∧ ((∀ k. Lt(k,h) → ∃ i. BetaAt(n,m,k,i) ∧ (i = 0 ∧ (Lt(q · S efrd_row_index_fubini_row_split_exists_previous,p · S k) ∧ ¬Lt(p · S k,q · S efrd_row_index_fubini_row_split_exists_previous)) ∨ i = 1 ∧ (Lt(p · S k,q · S efrd_row_index_fubini_row_split_exists_previous) ∧ ¬Lt(q · S efrd_row_index_fubini_row_split_exists_previous,p · S k)))) ∧ BetaAt(n,m,h,z)) ∧ (BitCount(n,m,h,y) ∧ (z = 0 ∨ z = 1) ∧ x = y + z))Exact native replay line
have 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))))) - 0027
intro i - 0028
intro hi - 0029
specialize hchoices i - 0030
apply hchoices - 0031
specialize le_succ (S i) - 0032
specialize le_succ l - 0033
apply le_succ - 0034
exact hi - 0035
have hprevious_prefix : ∃ db. ∃ dc. ∃ tb. ∃ tc. ∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(bb,bc,x,y) ∧ BetaAt(db,dc,x,z) ∧ BetaAt(tb,tc,x,n) ∧ (∃ m. ∃ k. (∀ i. Lt(i,sh) → ∃ j. BetaAt(m,k,i,j) ∧ (j = 0 ∧ (Lt(q · S x,p · S i) ∧ ¬Lt(p · S i,q · S x)) ∨ j = 1 ∧ (Lt(p · S i,q · S x) ∧ ¬Lt(q · S x,p · S i)))) ∧ BitCount(m,k,sh,y) ∧ ((∀ i. Lt(i,h) → ∃ j. BetaAt(m,k,i,j) ∧ (j = 0 ∧ (Lt(q · S x,p · S i) ∧ ¬Lt(p · S i,q · S x)) ∨ j = 1 ∧ (Lt(p · S i,q · S x) ∧ ¬Lt(q · S x,p · S i)))) ∧ BetaAt(m,k,h,n)) ∧ (BitCount(m,k,h,z) ∧ (n = 0 ∨ n = 1) ∧ y = z + n))Exact native replay line
have 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))))))) - 0036
apply IH - 0037
exact hprevious_choices - 0038
cases hprevious_prefix - 0039
cases hprevious_prefix_witness - 0040
cases hprevious_prefix_witness_witness - 0041
cases hprevious_prefix_witness_witness_witness - 0042
have hlast : ∃ n. ∃ r. ∃ a. BetaAt(bb,bc,l,n) ∧ (∃ x. ∃ y. (∀ z. Lt(z,sh) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(q · S l,p · S z) ∧ ¬Lt(p · S z,q · S l)) ∨ m = 1 ∧ (Lt(p · S z,q · S l) ∧ ¬Lt(q · S l,p · S z)))) ∧ BitCount(x,y,sh,n) ∧ ((∀ z. Lt(z,h) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(q · S l,p · S z) ∧ ¬Lt(p · S z,q · S l)) ∨ m = 1 ∧ (Lt(p · S z,q · S l) ∧ ¬Lt(q · S l,p · S z)))) ∧ BetaAt(x,y,h,a)) ∧ (BitCount(x,y,h,r) ∧ (a = 0 ∨ a = 1) ∧ n = r + a))Exact native replay line
have 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))))) - 0043
specialize hchoices l - 0044
apply hchoices - 0045
specialize le_refl (S l) - 0046
exact le_refl - 0047
have hnext : ∃ db. ∃ dc. ∃ tb. ∃ tc. ∀ x. Lt(x,S l) → ∃ y. ∃ z. ∃ n. BetaAt(bb,bc,x,y) ∧ BetaAt(db,dc,x,z) ∧ BetaAt(tb,tc,x,n) ∧ (∃ m. ∃ k. (∀ i. Lt(i,sh) → ∃ j. BetaAt(m,k,i,j) ∧ (j = 0 ∧ (Lt(q · S x,p · S i) ∧ ¬Lt(p · S i,q · S x)) ∨ j = 1 ∧ (Lt(p · S i,q · S x) ∧ ¬Lt(q · S x,p · S i)))) ∧ BitCount(m,k,sh,y) ∧ ((∀ i. Lt(i,h) → ∃ j. BetaAt(m,k,i,j) ∧ (j = 0 ∧ (Lt(q · S x,p · S i) ∧ ¬Lt(p · S i,q · S x)) ∨ j = 1 ∧ (Lt(p · S i,q · S x) ∧ ¬Lt(q · S x,p · S i)))) ∧ BetaAt(m,k,h,n)) ∧ (BitCount(m,k,h,z) ∧ (n = 0 ∨ n = 1) ∧ y = z + n))Exact native replay line
have 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))))))) - 0048
specialize eisenstein_successor_row_split_prefix_extend p - 0049
specialize eisenstein_successor_row_split_prefix_extend q - 0050
specialize eisenstein_successor_row_split_prefix_extend h - 0051
specialize eisenstein_successor_row_split_prefix_extend sh - 0052
specialize eisenstein_successor_row_split_prefix_extend bb - 0053
specialize eisenstein_successor_row_split_prefix_extend bc - 0054
specialize eisenstein_successor_row_split_prefix_extend x - 0055
specialize eisenstein_successor_row_split_prefix_extend x1 - 0056
specialize eisenstein_successor_row_split_prefix_extend x2 - 0057
specialize eisenstein_successor_row_split_prefix_extend x3 - 0058
specialize eisenstein_successor_row_split_prefix_extend l - 0059
apply eisenstein_successor_row_split_prefix_extend - 0060
exact hprevious_prefix_witness_witness_witness_witness - 0061
exact hlast - 0062
exact hnext