PA00EV · theorem

eisenstein_successor_row_split_choices

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

Every stored successor row constructively chooses an aligned reduced count and terminal bit.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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. 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))

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

26 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0017 BitCount

23 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))))))))) -> (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))))))

Proof neighborhood

Direct theorem prerequisites

PA00EU eisenstein_successor_row_count_decompose

Direct theorem dependents

PA00EY eisenstein_successor_rectangle_row_split_prefix_exists

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

35 script commands · 9 reading checkpoints · 2 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 (1)
eisenstein successor row count decompose
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro h
  4. L4
    intro sh
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro l
  8. L8
    intro hsh
  9. L9
    intro houter
  10. L10
    intro i
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hi
03Establish hstoredL12–15

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

  1. L12
    have hstored : ∃ n. BetaAt(bb,bc,i,n) ∧ (∃ x. ∃ y. (∀ z. Lt(z,sh) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ m = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))) ∧ BitCount(x,y,sh,n))Definitions: BetaAt(bb,bc,i,n)Lt(z,sh)BetaAt(x,y,z,m)Lt(q · S i,p · S z)Lt(p · S z,q · S i)BitCount(x,y,sh,n)Original native command in the exact edition
  2. L13
    specialize houter i
  3. L14
    apply houter
  4. L15
    exact hi
04Separate the logical casesL16–17

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

  1. L16
    cases hstored
  2. L17
    cases hstored_witness
05Establish hsplitL18–27

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

  1. L18
    have hsplit · expand full local formula (872 characters)have hsplit : ∃ efrd_terminal_bit_fubini_row_split_choices_decomposition. ∃ efrd_reduced_count_fubini_row_split_choices_decomposition. ∃ y. ∃ z. (∀ n. Lt(n,sh) → ∃ m. BetaAt(y,z,n,m) ∧ (m = 0 ∧ (Lt(q · S i,p · S n) ∧ ¬Lt(p · S n,q · S i)) ∨ m = 1 ∧ (Lt(p · S n,q · S i) ∧ ¬Lt(q · S i,p · S n)))) ∧ BitCount(y,z,sh,x) ∧ ((∀ n. Lt(n,h) → ∃ m. BetaAt(y,z,n,m) ∧ (m = 0 ∧ (Lt(q · S i,p · S n) ∧ ¬Lt(p · S n,q · S i)) ∨ m = 1 ∧ (Lt(p · S n,q · S i) ∧ ¬Lt(q · S i,p · S n)))) ∧ BetaAt(y,z,h,efrd_terminal_bit_fubini_row_split_choices_decomposition)) ∧ (BitCount(y,z,h,efrd_reduced_count_fubini_row_split_choices_decomposition) ∧ (efrd_terminal_bit_fubini_row_split_choices_decomposition = 0 ∨ efrd_terminal_bit_fubini_row_split_choices_decomposition = 1) ∧ x = efrd_reduced_count_fubini_row_split_choices_decomposition + efrd_terminal_bit_fubini_row_split_choices_decomposition)
    Definitions: Lt(n,sh)BetaAt(y,z,n,m)Lt(q · S i,p · S n)Lt(p · S n,q · S i)BitCount(y,z,sh,x)Lt(n,h)BetaAt(y,z,h,efrd_terminal_bit_fubini_row_split_choices_decomposition)BitCount(y,z,h,efrd_reduced_count_fubini_row_split_choices_decomposition)Original native command in the exact edition
  2. L19
    specialize eisenstein_successor_row_count_decompose p
  3. L20
    specialize eisenstein_successor_row_count_decompose q
  4. L21
    specialize eisenstein_successor_row_count_decompose h
  5. L22
    specialize eisenstein_successor_row_count_decompose sh
  6. L23
    specialize eisenstein_successor_row_count_decompose i
  7. L24
    specialize eisenstein_successor_row_count_decompose x
  8. L25
    apply eisenstein_successor_row_count_decompose
  9. L26
    exact hsh
  10. L27
    exact hstored_witness_right
06Separate the logical casesL28–29

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

  1. L28
    cases hsplit
  2. L29
    cases hsplit_witness
07Construct an explicit witnessL30–32

Supply the displayed value, then prove that it has the required property.

  1. L30
    exists x
  2. L31
    exists x2
  3. L32
    exists x1
08Separate the logical casesL33–33

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

  1. L33
    split
09Use earlier factsL34–35

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

  1. L34
    exact hstored_witness_left
  2. L35
    exact hsplit_witness_witness

Library-wide reading audit

Original defined command ledger · 35 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. 0010intro i
  11. 0011intro hi
  12. 0012have hstored : ∃ n. BetaAt(bb,bc,i,n) ∧ (∃ x. ∃ y. (∀ z. Lt(z,sh) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ m = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))) ∧ BitCount(x,y,sh,n))
    Exact native replay linehave hstored : exists n. ((((exists ff_h_fubini_row_split_choices_stored_entry. ff_h_fubini_row_split_choices_stored_entry + S (n) = S ((S (i)) * bc)) /\ exists ff_q_fubini_row_split_choices_stored_entry. bb = ff_q_fubini_row_split_choices_stored_entry * S ((S (i)) * bc) + (n))) /\ (exists erc_row_code_fubini_row_split_choices_stored_witness erc_row_scale_fubini_row_split_choices_stored_witness. ((forall eri_column_erc_fubini_row_split_choices_stored_witness_row. (exists eri_gap_erc_fubini_row_split_choices_stored_witness_row_bound. eri_gap_erc_fubini_row_split_choices_stored_witness_row_bound + S (eri_column_erc_fubini_row_split_choices_stored_witness_row) = sh) -> exists eri_bit_erc_fubini_row_split_choices_stored_witness_row. ((((exists ff_h_eri_erc_fubini_row_split_choices_stored_witness_row_decoded. ff_h_eri_erc_fubini_row_split_choices_stored_witness_row_decoded + S (eri_bit_erc_fubini_row_split_choices_stored_witness_row) = S ((S (eri_column_erc_fubini_row_split_choices_stored_witness_row)) * erc_row_scale_fubini_row_split_choices_stored_witness)) /\ exists ff_q_eri_erc_fubini_row_split_choices_stored_witness_row_decoded. erc_row_code_fubini_row_split_choices_stored_witness = ff_q_eri_erc_fubini_row_split_choices_stored_witness_row_decoded * S ((S (eri_column_erc_fubini_row_split_choices_stored_witness_row)) * erc_row_scale_fubini_row_split_choices_stored_witness) + (eri_bit_erc_fubini_row_split_choices_stored_witness_row))) /\ (((eri_bit_erc_fubini_row_split_choices_stored_witness_row = 0 /\ ((exists eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_left. eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_fubini_row_split_choices_stored_witness_row) /\ ~(exists eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_right. eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_right + S (p * S eri_column_erc_fubini_row_split_choices_stored_witness_row) = q * S i))) \/ (eri_bit_erc_fubini_row_split_choices_stored_witness_row = 1 /\ ((exists eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_right. eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_right + S (p * S eri_column_erc_fubini_row_split_choices_stored_witness_row) = q * S i) /\ ~(exists eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_left. eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_fubini_row_split_choices_stored_witness_row))))))) /\ (((exists ff_u_erc_fubini_row_split_choices_stored_witness_count_sum ff_v_erc_fubini_row_split_choices_stored_witness_count_sum. ((((exists ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_start. ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum)) /\ exists ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_start. ff_u_erc_fubini_row_split_choices_stored_witness_count_sum = ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_terminal. ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_terminal + S (n) = S ((S (sh)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum)) /\ exists ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_terminal. ff_u_erc_fubini_row_split_choices_stored_witness_count_sum = ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_terminal * S ((S (sh)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum) + (n))) /\ forall ff_i_erc_fubini_row_split_choices_stored_witness_count_sum. (exists ff_lt_erc_fubini_row_split_choices_stored_witness_count_sum_bound. ff_lt_erc_fubini_row_split_choices_stored_witness_count_sum_bound + S ff_i_erc_fubini_row_split_choices_stored_witness_count_sum = sh) -> exists ff_a_erc_fubini_row_split_choices_stored_witness_count_sum ff_r_erc_fubini_row_split_choices_stored_witness_count_sum ff_s_erc_fubini_row_split_choices_stored_witness_count_sum. ((((exists ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_summand. ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_summand + S (ff_a_erc_fubini_row_split_choices_stored_witness_count_sum) = S ((S (ff_i_erc_fubini_row_split_choices_stored_witness_count_sum)) * erc_row_scale_fubini_row_split_choices_stored_witness)) /\ exists ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_summand. erc_row_code_fubini_row_split_choices_stored_witness = ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_summand * S ((S (ff_i_erc_fubini_row_split_choices_stored_witness_count_sum)) * erc_row_scale_fubini_row_split_choices_stored_witness) + (ff_a_erc_fubini_row_split_choices_stored_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_partial. ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_partial + S (ff_r_erc_fubini_row_split_choices_stored_witness_count_sum) = S ((S (ff_i_erc_fubini_row_split_choices_stored_witness_count_sum)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum)) /\ exists ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_partial. ff_u_erc_fubini_row_split_choices_stored_witness_count_sum = ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_partial * S ((S (ff_i_erc_fubini_row_split_choices_stored_witness_count_sum)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum) + (ff_r_erc_fubini_row_split_choices_stored_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_successor. ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_successor + S (ff_s_erc_fubini_row_split_choices_stored_witness_count_sum) = S ((S (S ff_i_erc_fubini_row_split_choices_stored_witness_count_sum)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum)) /\ exists ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_successor. ff_u_erc_fubini_row_split_choices_stored_witness_count_sum = ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_row_split_choices_stored_witness_count_sum)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum) + (ff_s_erc_fubini_row_split_choices_stored_witness_count_sum))) /\ ff_s_erc_fubini_row_split_choices_stored_witness_count_sum = ff_r_erc_fubini_row_split_choices_stored_witness_count_sum + ff_a_erc_fubini_row_split_choices_stored_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_row_split_choices_stored_witness_count_bits. (exists ff_lt_erc_fubini_row_split_choices_stored_witness_count_bits_bound. ff_lt_erc_fubini_row_split_choices_stored_witness_count_bits_bound + S ff_i_erc_fubini_row_split_choices_stored_witness_count_bits = sh) -> exists ff_bit_erc_fubini_row_split_choices_stored_witness_count_bits. ((((exists ff_h_erc_fubini_row_split_choices_stored_witness_count_bits_decoded. ff_h_erc_fubini_row_split_choices_stored_witness_count_bits_decoded + S (ff_bit_erc_fubini_row_split_choices_stored_witness_count_bits) = S ((S (ff_i_erc_fubini_row_split_choices_stored_witness_count_bits)) * erc_row_scale_fubini_row_split_choices_stored_witness)) /\ exists ff_q_erc_fubini_row_split_choices_stored_witness_count_bits_decoded. erc_row_code_fubini_row_split_choices_stored_witness = ff_q_erc_fubini_row_split_choices_stored_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_row_split_choices_stored_witness_count_bits)) * erc_row_scale_fubini_row_split_choices_stored_witness) + (ff_bit_erc_fubini_row_split_choices_stored_witness_count_bits))) /\ (ff_bit_erc_fubini_row_split_choices_stored_witness_count_bits = 0 \/ ff_bit_erc_fubini_row_split_choices_stored_witness_count_bits = 1))))))))
  13. 0013specialize houter i
  14. 0014apply houter
  15. 0015exact hi
  16. 0016cases hstored
  17. 0017cases hstored_witness
  18. 0018have hsplit : ∃ efrd_terminal_bit_fubini_row_split_choices_decomposition. ∃ efrd_reduced_count_fubini_row_split_choices_decomposition. ∃ y. ∃ z. (∀ n. Lt(n,sh) → ∃ m. BetaAt(y,z,n,m) ∧ (m = 0 ∧ (Lt(q · S i,p · S n) ∧ ¬Lt(p · S n,q · S i)) ∨ m = 1 ∧ (Lt(p · S n,q · S i) ∧ ¬Lt(q · S i,p · S n)))) ∧ BitCount(y,z,sh,x) ∧ ((∀ n. Lt(n,h) → ∃ m. BetaAt(y,z,n,m) ∧ (m = 0 ∧ (Lt(q · S i,p · S n) ∧ ¬Lt(p · S n,q · S i)) ∨ m = 1 ∧ (Lt(p · S n,q · S i) ∧ ¬Lt(q · S i,p · S n)))) ∧ BetaAt(y,z,h,efrd_terminal_bit_fubini_row_split_choices_decomposition)) ∧ (BitCount(y,z,h,efrd_reduced_count_fubini_row_split_choices_decomposition) ∧ (efrd_terminal_bit_fubini_row_split_choices_decomposition = 0 ∨ efrd_terminal_bit_fubini_row_split_choices_decomposition = 1) ∧ x = efrd_reduced_count_fubini_row_split_choices_decomposition + efrd_terminal_bit_fubini_row_split_choices_decomposition)
    Exact native replay linehave hsplit : exists efrd_terminal_bit_fubini_row_split_choices_decomposition efrd_reduced_count_fubini_row_split_choices_decomposition. (exists efrd_row_code_fubini_row_split_choices_decomposition_split efrd_row_scale_fubini_row_split_choices_decomposition_split. (((((forall eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix. (exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_bound. eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_choices_decomposition_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_choices_decomposition_split_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_eri_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_decoded. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_eri_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (eri_bit_efrd_fubini_row_split_choices_decomposition_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_choices_decomposition_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix) = q * S i))) \/ (eri_bit_efrd_fubini_row_split_choices_decomposition_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix) = q * S i) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_start. ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_start. ff_u_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_terminal + S (x) = S ((S (sh)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) + (x))) /\ forall ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum ff_r_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum ff_s_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_summand. ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_summand. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (ff_a_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_partial. ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_partial. ff_u_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) + (ff_r_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_successor. ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_successor. ff_u_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) + (ff_s_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum = ff_r_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum + ff_a_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits_decoded. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (ff_bit_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_eri_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_decoded. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_eri_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (eri_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix) = q * S i))) \/ (eri_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix) = q * S i) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_terminal_entry. ff_h_efrd_fubini_row_split_choices_decomposition_split_terminal_entry + S (efrd_terminal_bit_fubini_row_split_choices_decomposition) = S ((S (h)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_terminal_entry. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_efrd_fubini_row_split_choices_decomposition_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (efrd_terminal_bit_fubini_row_split_choices_decomposition))))) /\ (((((exists ff_u_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_start. ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_start. ff_u_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_row_split_choices_decomposition) = S ((S (h)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) + (efrd_reduced_count_fubini_row_split_choices_decomposition))) /\ forall ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum ff_r_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum ff_s_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_summand. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (ff_a_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) + (ff_r_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) + (ff_s_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum = ff_r_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum + ff_a_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (ff_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_row_split_choices_decomposition = 0 \/ efrd_terminal_bit_fubini_row_split_choices_decomposition = 1)) /\ x = efrd_reduced_count_fubini_row_split_choices_decomposition + efrd_terminal_bit_fubini_row_split_choices_decomposition))))
  19. 0019specialize eisenstein_successor_row_count_decompose p
  20. 0020specialize eisenstein_successor_row_count_decompose q
  21. 0021specialize eisenstein_successor_row_count_decompose h
  22. 0022specialize eisenstein_successor_row_count_decompose sh
  23. 0023specialize eisenstein_successor_row_count_decompose i
  24. 0024specialize eisenstein_successor_row_count_decompose x
  25. 0025apply eisenstein_successor_row_count_decompose
  26. 0026exact hsh
  27. 0027exact hstored_witness_right
  28. 0028cases hsplit
  29. 0029cases hsplit_witness
  30. 0030exists x
  31. 0031exists x2
  32. 0032exists x1
  33. 0033split
  34. 0034exact hstored_witness_left
  35. 0035exact hsplit_witness_witness