PA00EY · theorem

eisenstein_successor_rectangle_row_split_prefix_exists

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

A semantic successor-width rectangle yields aligned reduced-count and terminal-bit β-prefixes.

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. sh = S h → (∀ x. Lt(x,l) → ∃ y. BetaAt(bb,bc,x,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,sh) → ∃ k. BetaAt(z,n,m,k) ∧ (k = 0 ∧ (Lt(q · S x,p · S m) ∧ ¬Lt(p · S m,q · S x)) ∨ k = 1 ∧ (Lt(p · S m,q · S x) ∧ ¬Lt(q · S x,p · S m)))) ∧ BitCount(z,n,sh,y))) → ∃ 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

PD0002 Lt PD0013 BetaAt PD0017 BitCount

28 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0017 BitCount

17 occurrences

Exact expanded native-PA statement
forall p q h sh bb bc l. sh = S h -> (forall erc_row_fubini_outer_decompose_prefix. (exists erc_lt_gap_fubini_outer_decompose_prefix_bound. erc_lt_gap_fubini_outer_decompose_prefix_bound + S (erc_row_fubini_outer_decompose_prefix) = l) -> exists erc_count_fubini_outer_decompose_prefix. ((((exists ff_h_erc_fubini_outer_decompose_prefix_decoded. ff_h_erc_fubini_outer_decompose_prefix_decoded + S (erc_count_fubini_outer_decompose_prefix) = S ((S (erc_row_fubini_outer_decompose_prefix)) * bc)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_decoded. bb = ff_q_erc_fubini_outer_decompose_prefix_decoded * S ((S (erc_row_fubini_outer_decompose_prefix)) * bc) + (erc_count_fubini_outer_decompose_prefix))) /\ (exists erc_row_code_fubini_outer_decompose_prefix_witness erc_row_scale_fubini_outer_decompose_prefix_witness. ((forall eri_column_erc_fubini_outer_decompose_prefix_witness_row. (exists eri_gap_erc_fubini_outer_decompose_prefix_witness_row_bound. eri_gap_erc_fubini_outer_decompose_prefix_witness_row_bound + S (eri_column_erc_fubini_outer_decompose_prefix_witness_row) = sh) -> exists eri_bit_erc_fubini_outer_decompose_prefix_witness_row. ((((exists ff_h_eri_erc_fubini_outer_decompose_prefix_witness_row_decoded. ff_h_eri_erc_fubini_outer_decompose_prefix_witness_row_decoded + S (eri_bit_erc_fubini_outer_decompose_prefix_witness_row) = S ((S (eri_column_erc_fubini_outer_decompose_prefix_witness_row)) * erc_row_scale_fubini_outer_decompose_prefix_witness)) /\ exists ff_q_eri_erc_fubini_outer_decompose_prefix_witness_row_decoded. erc_row_code_fubini_outer_decompose_prefix_witness = ff_q_eri_erc_fubini_outer_decompose_prefix_witness_row_decoded * S ((S (eri_column_erc_fubini_outer_decompose_prefix_witness_row)) * erc_row_scale_fubini_outer_decompose_prefix_witness) + (eri_bit_erc_fubini_outer_decompose_prefix_witness_row))) /\ (((eri_bit_erc_fubini_outer_decompose_prefix_witness_row = 0 /\ ((exists eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_left. eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_left + S (q * S erc_row_fubini_outer_decompose_prefix) = p * S eri_column_erc_fubini_outer_decompose_prefix_witness_row) /\ ~(exists eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_right. eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_right + S (p * S eri_column_erc_fubini_outer_decompose_prefix_witness_row) = q * S erc_row_fubini_outer_decompose_prefix))) \/ (eri_bit_erc_fubini_outer_decompose_prefix_witness_row = 1 /\ ((exists eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_right. eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_right + S (p * S eri_column_erc_fubini_outer_decompose_prefix_witness_row) = q * S erc_row_fubini_outer_decompose_prefix) /\ ~(exists eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_left. eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_left + S (q * S erc_row_fubini_outer_decompose_prefix) = p * S eri_column_erc_fubini_outer_decompose_prefix_witness_row))))))) /\ (((exists ff_u_erc_fubini_outer_decompose_prefix_witness_count_sum ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum. ((((exists ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_start. ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_start. ff_u_erc_fubini_outer_decompose_prefix_witness_count_sum = ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_terminal. ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_terminal + S (erc_count_fubini_outer_decompose_prefix) = S ((S (sh)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_terminal. ff_u_erc_fubini_outer_decompose_prefix_witness_count_sum = ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_terminal * S ((S (sh)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum) + (erc_count_fubini_outer_decompose_prefix))) /\ forall ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum. (exists ff_lt_erc_fubini_outer_decompose_prefix_witness_count_sum_bound. ff_lt_erc_fubini_outer_decompose_prefix_witness_count_sum_bound + S ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum = sh) -> exists ff_a_erc_fubini_outer_decompose_prefix_witness_count_sum ff_r_erc_fubini_outer_decompose_prefix_witness_count_sum ff_s_erc_fubini_outer_decompose_prefix_witness_count_sum. ((((exists ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_summand. ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_summand + S (ff_a_erc_fubini_outer_decompose_prefix_witness_count_sum) = S ((S (ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum)) * erc_row_scale_fubini_outer_decompose_prefix_witness)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_summand. erc_row_code_fubini_outer_decompose_prefix_witness = ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_summand * S ((S (ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum)) * erc_row_scale_fubini_outer_decompose_prefix_witness) + (ff_a_erc_fubini_outer_decompose_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_partial. ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_partial + S (ff_r_erc_fubini_outer_decompose_prefix_witness_count_sum) = S ((S (ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_partial. ff_u_erc_fubini_outer_decompose_prefix_witness_count_sum = ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_partial * S ((S (ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum) + (ff_r_erc_fubini_outer_decompose_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_successor. ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_successor + S (ff_s_erc_fubini_outer_decompose_prefix_witness_count_sum) = S ((S (S ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_successor. ff_u_erc_fubini_outer_decompose_prefix_witness_count_sum = ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum) + (ff_s_erc_fubini_outer_decompose_prefix_witness_count_sum))) /\ ff_s_erc_fubini_outer_decompose_prefix_witness_count_sum = ff_r_erc_fubini_outer_decompose_prefix_witness_count_sum + ff_a_erc_fubini_outer_decompose_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_outer_decompose_prefix_witness_count_bits. (exists ff_lt_erc_fubini_outer_decompose_prefix_witness_count_bits_bound. ff_lt_erc_fubini_outer_decompose_prefix_witness_count_bits_bound + S ff_i_erc_fubini_outer_decompose_prefix_witness_count_bits = sh) -> exists ff_bit_erc_fubini_outer_decompose_prefix_witness_count_bits. ((((exists ff_h_erc_fubini_outer_decompose_prefix_witness_count_bits_decoded. ff_h_erc_fubini_outer_decompose_prefix_witness_count_bits_decoded + S (ff_bit_erc_fubini_outer_decompose_prefix_witness_count_bits) = S ((S (ff_i_erc_fubini_outer_decompose_prefix_witness_count_bits)) * erc_row_scale_fubini_outer_decompose_prefix_witness)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_witness_count_bits_decoded. erc_row_code_fubini_outer_decompose_prefix_witness = ff_q_erc_fubini_outer_decompose_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_outer_decompose_prefix_witness_count_bits)) * erc_row_scale_fubini_outer_decompose_prefix_witness) + (ff_bit_erc_fubini_outer_decompose_prefix_witness_count_bits))) /\ (ff_bit_erc_fubini_outer_decompose_prefix_witness_count_bits = 0 \/ ff_bit_erc_fubini_outer_decompose_prefix_witness_count_bits = 1))))))))) -> (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

PA00EV eisenstein_successor_row_split_choices PA00EX eisenstein_successor_row_split_prefix_exists

Direct theorem dependents

PA00FC eisenstein_fubini_universal

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

29 script commands · 3 reading checkpoints · 1 local claims

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

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
eisenstein successor row split choiceseisenstein successor row split prefix exists
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro h
  4. L4
    intro sh
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro l
  8. L8
    intro hsh
  9. L9
    intro houter
02Establish hchoicesL10–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein successor row split choices.

  1. L10
    have hchoices · expand full local formula (891 characters)have hchoices : ∀ efrd_row_index_fubini_row_split_choices. Lt(efrd_row_index_fubini_row_split_choices,l) → ∃ x. ∃ y. ∃ z. BetaAt(bb,bc,efrd_row_index_fubini_row_split_choices,x) ∧ (∃ n. ∃ m. (∀ k. Lt(k,sh) → ∃ i. BetaAt(n,m,k,i) ∧ (i = 0 ∧ (Lt(q · S efrd_row_index_fubini_row_split_choices,p · S k) ∧ ¬Lt(p · S k,q · S efrd_row_index_fubini_row_split_choices)) ∨ i = 1 ∧ (Lt(p · S k,q · S efrd_row_index_fubini_row_split_choices) ∧ ¬Lt(q · S efrd_row_index_fubini_row_split_choices,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_choices,p · S k) ∧ ¬Lt(p · S k,q · S efrd_row_index_fubini_row_split_choices)) ∨ i = 1 ∧ (Lt(p · S k,q · S efrd_row_index_fubini_row_split_choices) ∧ ¬Lt(q · S efrd_row_index_fubini_row_split_choices,p · S k)))) ∧ BetaAt(n,m,h,z)) ∧ (BitCount(n,m,h,y) ∧ (z = 0 ∨ z = 1) ∧ x = y + z))
    Definitions: Lt(efrd_row_index_fubini_row_split_choices,l)BetaAt(bb,bc,efrd_row_index_fubini_row_split_choices,x)Lt(k,sh)BetaAt(n,m,k,i)Lt(q · S efrd_row_index_fubini_row_split_choices,p · S k)Lt(p · S k,q · S efrd_row_index_fubini_row_split_choices)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
  2. L11
    specialize eisenstein_successor_row_split_choices p
  3. L12
    specialize eisenstein_successor_row_split_choices q
  4. L13
    specialize eisenstein_successor_row_split_choices h
  5. L14
    specialize eisenstein_successor_row_split_choices sh
  6. L15
    specialize eisenstein_successor_row_split_choices bb
  7. L16
    specialize eisenstein_successor_row_split_choices bc
  8. L17
    specialize eisenstein_successor_row_split_choices l
  9. L18
    apply eisenstein_successor_row_split_choices
  10. L19
    exact hsh
03Use earlier factsL20–29

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

  1. L20
    exact houter
  2. L21
    specialize eisenstein_successor_row_split_prefix_exists p
  3. L22
    specialize eisenstein_successor_row_split_prefix_exists q
  4. L23
    specialize eisenstein_successor_row_split_prefix_exists h
  5. L24
    specialize eisenstein_successor_row_split_prefix_exists sh
  6. L25
    specialize eisenstein_successor_row_split_prefix_exists bb
  7. L26
    specialize eisenstein_successor_row_split_prefix_exists bc
  8. L27
    specialize eisenstein_successor_row_split_prefix_exists l
  9. L28
    apply eisenstein_successor_row_split_prefix_exists
  10. L29
    exact hchoices

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro sh
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro l
  8. 0008intro hsh
  9. 0009intro houter
  10. 0010have hchoices : ∀ efrd_row_index_fubini_row_split_choices. Lt(efrd_row_index_fubini_row_split_choices,l) → ∃ x. ∃ y. ∃ z. BetaAt(bb,bc,efrd_row_index_fubini_row_split_choices,x) ∧ (∃ n. ∃ m. (∀ k. Lt(k,sh) → ∃ i. BetaAt(n,m,k,i) ∧ (i = 0 ∧ (Lt(q · S efrd_row_index_fubini_row_split_choices,p · S k) ∧ ¬Lt(p · S k,q · S efrd_row_index_fubini_row_split_choices)) ∨ i = 1 ∧ (Lt(p · S k,q · S efrd_row_index_fubini_row_split_choices) ∧ ¬Lt(q · S efrd_row_index_fubini_row_split_choices,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_choices,p · S k) ∧ ¬Lt(p · S k,q · S efrd_row_index_fubini_row_split_choices)) ∨ i = 1 ∧ (Lt(p · S k,q · S efrd_row_index_fubini_row_split_choices) ∧ ¬Lt(q · S efrd_row_index_fubini_row_split_choices,p · S k)))) ∧ BetaAt(n,m,h,z)) ∧ (BitCount(n,m,h,y) ∧ (z = 0 ∨ z = 1) ∧ x = y + z))
    Exact native replay linehave hchoices : forall efrd_row_index_fubini_row_split_choices. (exists efrd_lt_gap_fubini_row_split_choices_bound. efrd_lt_gap_fubini_row_split_choices_bound + S (efrd_row_index_fubini_row_split_choices) = l) -> exists efrd_count_fubini_row_split_choices efrd_reduced_count_fubini_row_split_choices efrd_terminal_bit_fubini_row_split_choices. ((((exists ff_h_efrd_fubini_row_split_choices_outer_entry. ff_h_efrd_fubini_row_split_choices_outer_entry + S (efrd_count_fubini_row_split_choices) = S ((S (efrd_row_index_fubini_row_split_choices)) * bc)) /\ exists ff_q_efrd_fubini_row_split_choices_outer_entry. bb = ff_q_efrd_fubini_row_split_choices_outer_entry * S ((S (efrd_row_index_fubini_row_split_choices)) * bc) + (efrd_count_fubini_row_split_choices))) /\ (exists efrd_row_code_fubini_row_split_choices_split efrd_row_scale_fubini_row_split_choices_split. (((((forall eri_column_efrd_fubini_row_split_choices_split_successor_prefix. (exists eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_bound. eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_choices_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_choices_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_choices_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_choices_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_choices_split_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_choices_split_successor_prefix)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_eri_efrd_fubini_row_split_choices_split_successor_prefix_decoded. efrd_row_code_fubini_row_split_choices_split = ff_q_eri_efrd_fubini_row_split_choices_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_choices_split_successor_prefix)) * efrd_row_scale_fubini_row_split_choices_split) + (eri_bit_efrd_fubini_row_split_choices_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_choices_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_choices) = p * S eri_column_efrd_fubini_row_split_choices_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_choices))) \/ (eri_bit_efrd_fubini_row_split_choices_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_choices) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_choices) = p * S eri_column_efrd_fubini_row_split_choices_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_choices_split_successor_count_sum ff_v_efrd_fubini_row_split_choices_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_start. ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_start. ff_u_efrd_fubini_row_split_choices_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_terminal + S (efrd_count_fubini_row_split_choices) = S ((S (sh)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_choices_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum) + (efrd_count_fubini_row_split_choices))) /\ forall ff_i_efrd_fubini_row_split_choices_split_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_choices_split_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_choices_split_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_choices_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_choices_split_successor_count_sum ff_r_efrd_fubini_row_split_choices_split_successor_count_sum ff_s_efrd_fubini_row_split_choices_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_summand. ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_choices_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_summand. efrd_row_code_fubini_row_split_choices_split = ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_choices_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_choices_split) + (ff_a_efrd_fubini_row_split_choices_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_partial. ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_choices_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_partial. ff_u_efrd_fubini_row_split_choices_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_choices_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum) + (ff_r_efrd_fubini_row_split_choices_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_successor. ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_choices_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_choices_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_successor. ff_u_efrd_fubini_row_split_choices_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_choices_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum) + (ff_s_efrd_fubini_row_split_choices_split_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_choices_split_successor_count_sum = ff_r_efrd_fubini_row_split_choices_split_successor_count_sum + ff_a_efrd_fubini_row_split_choices_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_choices_split_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_choices_split_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_choices_split_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_choices_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_choices_split_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_choices_split_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_choices_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_choices_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_choices_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_efrd_fubini_row_split_choices_split_successor_count_bits_decoded. efrd_row_code_fubini_row_split_choices_split = ff_q_efrd_fubini_row_split_choices_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_choices_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_choices_split) + (ff_bit_efrd_fubini_row_split_choices_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_choices_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_choices_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_choices_split_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_choices_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_choices_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_choices_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_choices_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_choices_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_choices_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_eri_efrd_fubini_row_split_choices_split_reduced_prefix_decoded. efrd_row_code_fubini_row_split_choices_split = ff_q_eri_efrd_fubini_row_split_choices_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_choices_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_choices_split) + (eri_bit_efrd_fubini_row_split_choices_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_choices_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_choices) = p * S eri_column_efrd_fubini_row_split_choices_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_choices))) \/ (eri_bit_efrd_fubini_row_split_choices_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_choices) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_choices) = p * S eri_column_efrd_fubini_row_split_choices_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_choices_split_terminal_entry. ff_h_efrd_fubini_row_split_choices_split_terminal_entry + S (efrd_terminal_bit_fubini_row_split_choices) = S ((S (h)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_efrd_fubini_row_split_choices_split_terminal_entry. efrd_row_code_fubini_row_split_choices_split = ff_q_efrd_fubini_row_split_choices_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_choices_split) + (efrd_terminal_bit_fubini_row_split_choices))))) /\ (((((exists ff_u_efrd_fubini_row_split_choices_split_reduced_count_sum ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_start. ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_start. ff_u_efrd_fubini_row_split_choices_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_row_split_choices) = S ((S (h)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_choices_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum) + (efrd_reduced_count_fubini_row_split_choices))) /\ forall ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_choices_split_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_choices_split_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_choices_split_reduced_count_sum ff_r_efrd_fubini_row_split_choices_split_reduced_count_sum ff_s_efrd_fubini_row_split_choices_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_choices_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_summand. efrd_row_code_fubini_row_split_choices_split = ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_choices_split) + (ff_a_efrd_fubini_row_split_choices_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_choices_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_choices_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum) + (ff_r_efrd_fubini_row_split_choices_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_choices_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_choices_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum) + (ff_s_efrd_fubini_row_split_choices_split_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_choices_split_reduced_count_sum = ff_r_efrd_fubini_row_split_choices_split_reduced_count_sum + ff_a_efrd_fubini_row_split_choices_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_choices_split_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_choices_split_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_choices_split_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_choices_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_choices_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_choices_split_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_choices_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_choices_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_choices_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_efrd_fubini_row_split_choices_split_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_choices_split = ff_q_efrd_fubini_row_split_choices_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_choices_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_choices_split) + (ff_bit_efrd_fubini_row_split_choices_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_choices_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_choices_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_row_split_choices = 0 \/ efrd_terminal_bit_fubini_row_split_choices = 1)) /\ efrd_count_fubini_row_split_choices = efrd_reduced_count_fubini_row_split_choices + efrd_terminal_bit_fubini_row_split_choices)))))
  11. 0011specialize eisenstein_successor_row_split_choices p
  12. 0012specialize eisenstein_successor_row_split_choices q
  13. 0013specialize eisenstein_successor_row_split_choices h
  14. 0014specialize eisenstein_successor_row_split_choices sh
  15. 0015specialize eisenstein_successor_row_split_choices bb
  16. 0016specialize eisenstein_successor_row_split_choices bc
  17. 0017specialize eisenstein_successor_row_split_choices l
  18. 0018apply eisenstein_successor_row_split_choices
  19. 0019exact hsh
  20. 0020exact houter
  21. 0021specialize eisenstein_successor_row_split_prefix_exists p
  22. 0022specialize eisenstein_successor_row_split_prefix_exists q
  23. 0023specialize eisenstein_successor_row_split_prefix_exists h
  24. 0024specialize eisenstein_successor_row_split_prefix_exists sh
  25. 0025specialize eisenstein_successor_row_split_prefix_exists bb
  26. 0026specialize eisenstein_successor_row_split_prefix_exists bc
  27. 0027specialize eisenstein_successor_row_split_prefix_exists l
  28. 0028apply eisenstein_successor_row_split_prefix_exists
  29. 0029exact hchoices