PA00F9 · theorem

eisenstein_successor_terminal_bit_matches_last_column

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

The terminal-bit prefix and the constructed last column decode the same bit at every bounded row.

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. ∀ db. ∀ dc. ∀ tb. ∀ tc. ∀ cb. ∀ cc. ∀ l. ∀ j. ∀ a. ∀ d. sh = S h → (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(bb,bc,x,y) ∧ BetaAt(db,dc,x,z) ∧ BetaAt(tb,tc,x,n) ∧ (∃ m. ∃ k. (∀ i. Lt(i,sh) → ∃ u. BetaAt(m,k,i,u) ∧ (u = 0 ∧ (Lt(p · S x,q · S i) ∧ ¬Lt(q · S i,p · S x)) ∨ u = 1 ∧ (Lt(q · S i,p · S x) ∧ ¬Lt(p · S x,q · S i)))) ∧ BitCount(m,k,sh,y) ∧ ((∀ i. Lt(i,h) → ∃ u. BetaAt(m,k,i,u) ∧ (u = 0 ∧ (Lt(p · S x,q · S i) ∧ ¬Lt(q · S i,p · S x)) ∨ u = 1 ∧ (Lt(q · S i,p · S x) ∧ ¬Lt(p · S x,q · S i)))) ∧ BetaAt(m,k,h,n)) ∧ (BitCount(m,k,h,z) ∧ (n = 0 ∨ n = 1) ∧ y = z + n))) → (∀ x. Lt(x,l) → ∃ y. BetaAt(cb,cc,x,y) ∧ (∃ z. ∃ n. ∃ m. BetaAt(bb,bc,x,z) ∧ (∀ k. Lt(k,sh) → ∃ i. BetaAt(n,m,k,i) ∧ (i = 0 ∧ (Lt(p · S x,q · S k) ∧ ¬Lt(q · S k,p · S x)) ∨ i = 1 ∧ (Lt(q · S k,p · S x) ∧ ¬Lt(p · S x,q · S k)))) ∧ BitCount(n,m,sh,z) ∧ BetaAt(n,m,h,y))) → Lt(j,l) → BetaAt(tb,tc,j,a) → BetaAt(cb,cc,j,d) → a = d

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

33 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0017 BitCount

37 occurrences

Exact expanded native-PA statement
forall p q h sh bb bc db dc tb tc cb cc l j a d. sh = S h -> (forall efrd_row_index_fubini_terminal_column_split_prefix. (exists efrd_lt_gap_fubini_terminal_column_split_prefix_bound. efrd_lt_gap_fubini_terminal_column_split_prefix_bound + S (efrd_row_index_fubini_terminal_column_split_prefix) = l) -> exists efrd_count_fubini_terminal_column_split_prefix efrd_reduced_count_fubini_terminal_column_split_prefix efrd_terminal_bit_fubini_terminal_column_split_prefix. (((((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_outer_entry. ff_h_efrd_fubini_terminal_column_split_prefix_entry_outer_entry + S (efrd_count_fubini_terminal_column_split_prefix) = S ((S (efrd_row_index_fubini_terminal_column_split_prefix)) * bc)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_outer_entry. bb = ff_q_efrd_fubini_terminal_column_split_prefix_entry_outer_entry * S ((S (efrd_row_index_fubini_terminal_column_split_prefix)) * bc) + (efrd_count_fubini_terminal_column_split_prefix))) /\ (((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_reduced_entry. ff_h_efrd_fubini_terminal_column_split_prefix_entry_reduced_entry + S (efrd_reduced_count_fubini_terminal_column_split_prefix) = S ((S (efrd_row_index_fubini_terminal_column_split_prefix)) * dc)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_reduced_entry. db = ff_q_efrd_fubini_terminal_column_split_prefix_entry_reduced_entry * S ((S (efrd_row_index_fubini_terminal_column_split_prefix)) * dc) + (efrd_reduced_count_fubini_terminal_column_split_prefix)))) /\ (((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_terminal_entry. ff_h_efrd_fubini_terminal_column_split_prefix_entry_terminal_entry + S (efrd_terminal_bit_fubini_terminal_column_split_prefix) = S ((S (efrd_row_index_fubini_terminal_column_split_prefix)) * tc)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_terminal_entry. tb = ff_q_efrd_fubini_terminal_column_split_prefix_entry_terminal_entry * S ((S (efrd_row_index_fubini_terminal_column_split_prefix)) * tc) + (efrd_terminal_bit_fubini_terminal_column_split_prefix)))) /\ (exists efrd_row_code_fubini_terminal_column_split_prefix_entry_split efrd_row_scale_fubini_terminal_column_split_prefix_entry_split. (((((forall eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix. (exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_bound. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_bound + S (eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix) = S ((S (eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_eri_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_decoded. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_eri_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_left + S (p * S efrd_row_index_fubini_terminal_column_split_prefix) = q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_right + S (q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix) = p * S efrd_row_index_fubini_terminal_column_split_prefix))) \/ (eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_right + S (q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix) = p * S efrd_row_index_fubini_terminal_column_split_prefix) /\ ~(exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_left + S (p * S efrd_row_index_fubini_terminal_column_split_prefix) = q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_start. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_start. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_terminal. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_terminal + S (efrd_count_fubini_terminal_column_split_prefix) = S ((S (sh)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_terminal. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) + (efrd_count_fubini_terminal_column_split_prefix))) /\ forall ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum. (exists ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_bound. ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_bound + S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_summand. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_summand + S (ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_summand. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_partial. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_partial + S (ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_partial. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) + (ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_successor. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_successor + S (ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_successor. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) + (ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum))) /\ ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum = ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum + ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits. (exists ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits_bound. ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits_bound + S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits. ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits_decoded. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits_decoded. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix. (exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_bound. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_bound + S (eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_eri_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_decoded. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_eri_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_left + S (p * S efrd_row_index_fubini_terminal_column_split_prefix) = q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_right + S (q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix) = p * S efrd_row_index_fubini_terminal_column_split_prefix))) \/ (eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_right + S (q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix) = p * S efrd_row_index_fubini_terminal_column_split_prefix) /\ ~(exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_left + S (p * S efrd_row_index_fubini_terminal_column_split_prefix) = q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_terminal_entry. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_terminal_entry + S (efrd_terminal_bit_fubini_terminal_column_split_prefix) = S ((S (h)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_terminal_entry. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (efrd_terminal_bit_fubini_terminal_column_split_prefix))))) /\ (((((exists ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_start. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_start. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_terminal. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_terminal_column_split_prefix) = S ((S (h)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_terminal. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) + (efrd_reduced_count_fubini_terminal_column_split_prefix))) /\ forall ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum. (exists ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_bound. ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_bound + S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_summand. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_summand. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_partial. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_partial. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) + (ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_successor. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_successor. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) + (ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum))) /\ ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum = ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum + ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits. (exists ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits_bound. ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits_bound + S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits_decoded. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits_decoded. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_terminal_column_split_prefix = 0 \/ efrd_terminal_bit_fubini_terminal_column_split_prefix = 1)) /\ efrd_count_fubini_terminal_column_split_prefix = efrd_reduced_count_fubini_terminal_column_split_prefix + efrd_terminal_bit_fubini_terminal_column_split_prefix))))))) -> (forall etc_row_index_fubini_terminal_column_prefix. (exists edt_lt_gap_fubini_terminal_column_prefix_bound. edt_lt_gap_fubini_terminal_column_prefix_bound + S (etc_row_index_fubini_terminal_column_prefix) = l) -> exists etc_bit_fubini_terminal_column_prefix. ((((exists ff_h_etc_fubini_terminal_column_prefix_decoded. ff_h_etc_fubini_terminal_column_prefix_decoded + S (etc_bit_fubini_terminal_column_prefix) = S ((S (etc_row_index_fubini_terminal_column_prefix)) * cc)) /\ exists ff_q_etc_fubini_terminal_column_prefix_decoded. cb = ff_q_etc_fubini_terminal_column_prefix_decoded * S ((S (etc_row_index_fubini_terminal_column_prefix)) * cc) + (etc_bit_fubini_terminal_column_prefix))) /\ (exists etc_count_fubini_terminal_column_prefix_witness etc_row_code_fubini_terminal_column_prefix_witness etc_row_scale_fubini_terminal_column_prefix_witness. ((((((exists ff_h_etc_fubini_terminal_column_prefix_witness_outer_entry. ff_h_etc_fubini_terminal_column_prefix_witness_outer_entry + S (etc_count_fubini_terminal_column_prefix_witness) = S ((S (etc_row_index_fubini_terminal_column_prefix)) * bc)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_outer_entry. bb = ff_q_etc_fubini_terminal_column_prefix_witness_outer_entry * S ((S (etc_row_index_fubini_terminal_column_prefix)) * bc) + (etc_count_fubini_terminal_column_prefix_witness))) /\ (forall eri_column_etc_fubini_terminal_column_prefix_witness_row. (exists eri_gap_etc_fubini_terminal_column_prefix_witness_row_bound. eri_gap_etc_fubini_terminal_column_prefix_witness_row_bound + S (eri_column_etc_fubini_terminal_column_prefix_witness_row) = sh) -> exists eri_bit_etc_fubini_terminal_column_prefix_witness_row. ((((exists ff_h_eri_etc_fubini_terminal_column_prefix_witness_row_decoded. ff_h_eri_etc_fubini_terminal_column_prefix_witness_row_decoded + S (eri_bit_etc_fubini_terminal_column_prefix_witness_row) = S ((S (eri_column_etc_fubini_terminal_column_prefix_witness_row)) * etc_row_scale_fubini_terminal_column_prefix_witness)) /\ exists ff_q_eri_etc_fubini_terminal_column_prefix_witness_row_decoded. etc_row_code_fubini_terminal_column_prefix_witness = ff_q_eri_etc_fubini_terminal_column_prefix_witness_row_decoded * S ((S (eri_column_etc_fubini_terminal_column_prefix_witness_row)) * etc_row_scale_fubini_terminal_column_prefix_witness) + (eri_bit_etc_fubini_terminal_column_prefix_witness_row))) /\ (((eri_bit_etc_fubini_terminal_column_prefix_witness_row = 0 /\ ((exists eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_left. eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_left + S (p * S etc_row_index_fubini_terminal_column_prefix) = q * S eri_column_etc_fubini_terminal_column_prefix_witness_row) /\ ~(exists eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_right. eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_right + S (q * S eri_column_etc_fubini_terminal_column_prefix_witness_row) = p * S etc_row_index_fubini_terminal_column_prefix))) \/ (eri_bit_etc_fubini_terminal_column_prefix_witness_row = 1 /\ ((exists eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_right. eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_right + S (q * S eri_column_etc_fubini_terminal_column_prefix_witness_row) = p * S etc_row_index_fubini_terminal_column_prefix) /\ ~(exists eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_left. eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_left + S (p * S etc_row_index_fubini_terminal_column_prefix) = q * S eri_column_etc_fubini_terminal_column_prefix_witness_row)))))))) /\ (((exists ff_u_etc_fubini_terminal_column_prefix_witness_count_relation_sum ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum. ((((exists ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_start. ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_start. ff_u_etc_fubini_terminal_column_prefix_witness_count_relation_sum = ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_terminal. ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_terminal + S (etc_count_fubini_terminal_column_prefix_witness) = S ((S (sh)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_terminal. ff_u_etc_fubini_terminal_column_prefix_witness_count_relation_sum = ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_terminal * S ((S (sh)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum) + (etc_count_fubini_terminal_column_prefix_witness))) /\ forall ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum. (exists ff_lt_etc_fubini_terminal_column_prefix_witness_count_relation_sum_bound. ff_lt_etc_fubini_terminal_column_prefix_witness_count_relation_sum_bound + S ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum = sh) -> exists ff_a_etc_fubini_terminal_column_prefix_witness_count_relation_sum ff_r_etc_fubini_terminal_column_prefix_witness_count_relation_sum ff_s_etc_fubini_terminal_column_prefix_witness_count_relation_sum. ((((exists ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_summand. ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_summand + S (ff_a_etc_fubini_terminal_column_prefix_witness_count_relation_sum) = S ((S (ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) * etc_row_scale_fubini_terminal_column_prefix_witness)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_summand. etc_row_code_fubini_terminal_column_prefix_witness = ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_summand * S ((S (ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) * etc_row_scale_fubini_terminal_column_prefix_witness) + (ff_a_etc_fubini_terminal_column_prefix_witness_count_relation_sum))) /\ ((((exists ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_partial. ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_partial + S (ff_r_etc_fubini_terminal_column_prefix_witness_count_relation_sum) = S ((S (ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_partial. ff_u_etc_fubini_terminal_column_prefix_witness_count_relation_sum = ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_partial * S ((S (ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum) + (ff_r_etc_fubini_terminal_column_prefix_witness_count_relation_sum))) /\ ((((exists ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_successor. ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_successor + S (ff_s_etc_fubini_terminal_column_prefix_witness_count_relation_sum) = S ((S (S ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_successor. ff_u_etc_fubini_terminal_column_prefix_witness_count_relation_sum = ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_successor * S ((S (S ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum) + (ff_s_etc_fubini_terminal_column_prefix_witness_count_relation_sum))) /\ ff_s_etc_fubini_terminal_column_prefix_witness_count_relation_sum = ff_r_etc_fubini_terminal_column_prefix_witness_count_relation_sum + ff_a_etc_fubini_terminal_column_prefix_witness_count_relation_sum)))))) /\ (forall ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_bits. (exists ff_lt_etc_fubini_terminal_column_prefix_witness_count_relation_bits_bound. ff_lt_etc_fubini_terminal_column_prefix_witness_count_relation_bits_bound + S ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_bits = sh) -> exists ff_bit_etc_fubini_terminal_column_prefix_witness_count_relation_bits. ((((exists ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_bits_decoded. ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_bits_decoded + S (ff_bit_etc_fubini_terminal_column_prefix_witness_count_relation_bits) = S ((S (ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_bits)) * etc_row_scale_fubini_terminal_column_prefix_witness)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_bits_decoded. etc_row_code_fubini_terminal_column_prefix_witness = ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_bits_decoded * S ((S (ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_bits)) * etc_row_scale_fubini_terminal_column_prefix_witness) + (ff_bit_etc_fubini_terminal_column_prefix_witness_count_relation_bits))) /\ (ff_bit_etc_fubini_terminal_column_prefix_witness_count_relation_bits = 0 \/ ff_bit_etc_fubini_terminal_column_prefix_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_fubini_terminal_column_prefix_witness_inner_entry. ff_h_etc_fubini_terminal_column_prefix_witness_inner_entry + S (etc_bit_fubini_terminal_column_prefix) = S ((S (h)) * etc_row_scale_fubini_terminal_column_prefix_witness)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_inner_entry. etc_row_code_fubini_terminal_column_prefix_witness = ff_q_etc_fubini_terminal_column_prefix_witness_inner_entry * S ((S (h)) * etc_row_scale_fubini_terminal_column_prefix_witness) + (etc_bit_fubini_terminal_column_prefix))))))) -> (exists efrd_lt_gap_fubini_terminal_column_bound. efrd_lt_gap_fubini_terminal_column_bound + S (j) = l) -> (((exists ff_h_fubini_terminal_column_terminal_entry. ff_h_fubini_terminal_column_terminal_entry + S (a) = S ((S (j)) * tc)) /\ exists ff_q_fubini_terminal_column_terminal_entry. tb = ff_q_fubini_terminal_column_terminal_entry * S ((S (j)) * tc) + (a))) -> (((exists ff_h_fubini_terminal_column_column_entry. ff_h_fubini_terminal_column_column_entry + S (d) = S ((S (j)) * cc)) /\ exists ff_q_fubini_terminal_column_column_entry. cb = ff_q_fubini_terminal_column_column_entry * S ((S (j)) * cc) + (d))) -> a = d

Proof neighborhood

Direct theorem prerequisites

PA001A le_refl PA002F beta_at_unique PA00EA eisenstein_row_indicator_decoded_choice PA00F5 eisenstein_cell_indicator_choice_unique

Direct theorem dependents

PA00FA eisenstein_successor_terminal_prefix_to_last_column

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

111 script commands · 18 reading checkpoints · 7 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 (4)
le reflbeta at uniqueeisenstein row indicator decoded choiceeisenstein cell indicator choice unique
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 db
  8. L8
    intro dc
  9. L9
    intro tb
  10. L10
    intro tc
02Fix variables and assumptionsL11–20

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

  1. L11
    intro cb
  2. L12
    intro cc
  3. L13
    intro l
  4. L14
    intro j
  5. L15
    intro a
  6. L16
    intro d
  7. L17
    intro hsh
  8. L18
    intro hsplit
  9. L19
    intro hcolumn
  10. L20
    intro hj
03Fix variables and assumptionsL21–22

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

  1. L21
    intro ha
  2. L22
    intro hd
04Establish hhshL23–26

Establish this local claim before using it. It is not an additional assumption.

  1. L23
  2. L24
    rewrite hsh
  3. L25
    specialize le_refl (S h)
  4. L26
    exact le_refl
05Establish hsplit_storedL27–30

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

  1. L27
    have hsplit_stored : ∃ n. ∃ r. ∃ storeda. BetaAt(bb,bc,j,n) ∧ BetaAt(db,dc,j,r) ∧ BetaAt(tb,tc,j,storeda) ∧ (∃ x. ∃ y. (∀ z. Lt(z,sh) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(p · S j,q · S z) ∧ ¬Lt(q · S z,p · S j)) ∨ m = 1 ∧ (Lt(q · S z,p · S j) ∧ ¬Lt(p · S j,q · S z)))) ∧ BitCount(x,y,sh,n) ∧ ((∀ z. Lt(z,h) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(p · S j,q · S z) ∧ ¬Lt(q · S z,p · S j)) ∨ m = 1 ∧ (Lt(q · S z,p · S j) ∧ ¬Lt(p · S j,q · S z)))) ∧ BetaAt(x,y,h,storeda)) ∧ (BitCount(x,y,h,r) ∧ (storeda = 0 ∨ storeda = 1) ∧ n = r + storeda))Definitions: BetaAt(bb,bc,j,n)BetaAt(db,dc,j,r)BetaAt(tb,tc,j,storeda)Lt(z,sh)BetaAt(x,y,z,m)Lt(p · S j,q · S z)Lt(q · S z,p · S j)BitCount(x,y,sh,n)Lt(z,h)BetaAt(x,y,h,storeda)BitCount(x,y,h,r)Original native command in the exact edition
  2. L28
    specialize hsplit j
  3. L29
    apply hsplit
  4. L30
    exact hj
06Separate the logical casesL31–36

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

  1. L31
    cases hsplit_stored
  2. L32
    cases hsplit_stored_witness
  3. L33
    cases hsplit_stored_witness_witness
  4. L34
    cases hsplit_stored_witness_witness_witness
  5. L35
    cases hsplit_stored_witness_witness_witness_left
  6. L36
    cases hsplit_stored_witness_witness_witness_left_left
07Establish hstored_a_eqL37–45

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

  1. L37
    have hstored_a_eq : x2 = a
  2. L38
    specialize beta_at_unique tb
  3. L39
    specialize beta_at_unique tc
  4. L40
    specialize beta_at_unique j
  5. L41
    specialize beta_at_unique x2
  6. L42
    specialize beta_at_unique a
  7. L43
    apply beta_at_unique
  8. L44
    exact hsplit_stored_witness_witness_witness_left_right
  9. L45
    exact ha
08Separate the logical casesL46–51

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

  1. L46
    cases hsplit_stored_witness_witness_witness_right
  2. L47
    cases hsplit_stored_witness_witness_witness_right_witness
  3. L48
    cases hsplit_stored_witness_witness_witness_right_witness_witness
  4. L49
    cases hsplit_stored_witness_witness_witness_right_witness_witness_left
  5. L50
    cases hsplit_stored_witness_witness_witness_right_witness_witness_left_left
  6. L51
    cases hsplit_stored_witness_witness_witness_right_witness_witness_left_right
09Establish hterminal_choiceL52–61

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein row indicator decoded choice.

  1. L52
    have hterminal_choice : x2 = 0 ∧ (Lt(p · S j,q · S h) ∧ ¬Lt(q · S h,p · S j)) ∨ x2 = 1 ∧ (Lt(q · S h,p · S j) ∧ ¬Lt(p · S j,q · S h))Definitions: Lt(p · S j,q · S h)Lt(q · S h,p · S j)Original native command in the exact edition
  2. L53
    specialize eisenstein_row_indicator_decoded_choice q
  3. L54
    specialize eisenstein_row_indicator_decoded_choice p
  4. L55
    specialize eisenstein_row_indicator_decoded_choice j
  5. L56
    specialize eisenstein_row_indicator_decoded_choice x3
  6. L57
    specialize eisenstein_row_indicator_decoded_choice x4
  7. L58
    specialize eisenstein_row_indicator_decoded_choice sh
  8. L59
    specialize eisenstein_row_indicator_decoded_choice h
  9. L60
    specialize eisenstein_row_indicator_decoded_choice x2
  10. L61
    apply eisenstein_row_indicator_decoded_choice
10Use earlier factsL62–64

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

  1. L62
    exact hsplit_stored_witness_witness_witness_right_witness_witness_left_left_left
  2. L63
    exact hhsh
  3. L64
    exact hsplit_stored_witness_witness_witness_right_witness_witness_left_right_right
11Establish hcolumn_storedL65–68

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

  1. L65
    have hcolumn_stored : ∃ storedd. BetaAt(cb,cc,j,storedd) ∧ (∃ x. ∃ y. ∃ z. BetaAt(bb,bc,j,x) ∧ (∀ n. Lt(n,sh) → ∃ m. BetaAt(y,z,n,m) ∧ (m = 0 ∧ (Lt(p · S j,q · S n) ∧ ¬Lt(q · S n,p · S j)) ∨ m = 1 ∧ (Lt(q · S n,p · S j) ∧ ¬Lt(p · S j,q · S n)))) ∧ BitCount(y,z,sh,x) ∧ BetaAt(y,z,h,storedd))Definitions: BetaAt(cb,cc,j,storedd)BetaAt(bb,bc,j,x)Lt(n,sh)BetaAt(y,z,n,m)Lt(p · S j,q · S n)Lt(q · S n,p · S j)BitCount(y,z,sh,x)BetaAt(y,z,h,storedd)Original native command in the exact edition
  2. L66
    specialize hcolumn j
  3. L67
    apply hcolumn
  4. L68
    exact hj
12Separate the logical casesL69–70

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

  1. L69
    cases hcolumn_stored
  2. L70
    cases hcolumn_stored_witness
13Establish hstored_d_eqL71–79

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

  1. L71
    have hstored_d_eq : x5 = d
  2. L72
    specialize beta_at_unique cb
  3. L73
    specialize beta_at_unique cc
  4. L74
    specialize beta_at_unique j
  5. L75
    specialize beta_at_unique x5
  6. L76
    specialize beta_at_unique d
  7. L77
    apply beta_at_unique
  8. L78
    exact hcolumn_stored_witness_left
  9. L79
    exact hd
14Separate the logical casesL80–85

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

  1. L80
    cases hcolumn_stored_witness_right
  2. L81
    cases hcolumn_stored_witness_right_witness
  3. L82
    cases hcolumn_stored_witness_right_witness_witness
  4. L83
    cases hcolumn_stored_witness_right_witness_witness_witness
  5. L84
    cases hcolumn_stored_witness_right_witness_witness_witness_left
  6. L85
    cases hcolumn_stored_witness_right_witness_witness_witness_left_left
15Establish hcolumn_choiceL86–95

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein row indicator decoded choice.

  1. L86
    have hcolumn_choice : x5 = 0 ∧ (Lt(p · S j,q · S h) ∧ ¬Lt(q · S h,p · S j)) ∨ x5 = 1 ∧ (Lt(q · S h,p · S j) ∧ ¬Lt(p · S j,q · S h))Definitions: Lt(p · S j,q · S h)Lt(q · S h,p · S j)Original native command in the exact edition
  2. L87
    specialize eisenstein_row_indicator_decoded_choice q
  3. L88
    specialize eisenstein_row_indicator_decoded_choice p
  4. L89
    specialize eisenstein_row_indicator_decoded_choice j
  5. L90
    specialize eisenstein_row_indicator_decoded_choice x7
  6. L91
    specialize eisenstein_row_indicator_decoded_choice x8
  7. L92
    specialize eisenstein_row_indicator_decoded_choice sh
  8. L93
    specialize eisenstein_row_indicator_decoded_choice h
  9. L94
    specialize eisenstein_row_indicator_decoded_choice x5
  10. L95
    apply eisenstein_row_indicator_decoded_choice
16Use earlier factsL96–98

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

  1. L96
    exact hcolumn_stored_witness_right_witness_witness_witness_left_left_right
  2. L97
    exact hhsh
  3. L98
    exact hcolumn_stored_witness_right_witness_witness_witness_right
17Calculate and transport equalitiesL99–102

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L99
    rewrite hstored_a_eq at hterminal_choice
  2. L100
    rewrite hstored_a_eq at hterminal_choice
  3. L101
    rewrite hstored_d_eq at hcolumn_choice
  4. L102
    rewrite hstored_d_eq at hcolumn_choice
18Use earlier factsL103–111

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

  1. L103
    specialize eisenstein_cell_indicator_choice_unique q
  2. L104
    specialize eisenstein_cell_indicator_choice_unique p
  3. L105
    specialize eisenstein_cell_indicator_choice_unique j
  4. L106
    specialize eisenstein_cell_indicator_choice_unique h
  5. L107
    specialize eisenstein_cell_indicator_choice_unique a
  6. L108
    specialize eisenstein_cell_indicator_choice_unique d
  7. L109
    apply eisenstein_cell_indicator_choice_unique
  8. L110
    exact hterminal_choice
  9. L111
    exact hcolumn_choice

Library-wide reading audit

Original defined command ledger · 111 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro sh
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro db
  8. 0008intro dc
  9. 0009intro tb
  10. 0010intro tc
  11. 0011intro cb
  12. 0012intro cc
  13. 0013intro l
  14. 0014intro j
  15. 0015intro a
  16. 0016intro d
  17. 0017intro hsh
  18. 0018intro hsplit
  19. 0019intro hcolumn
  20. 0020intro hj
  21. 0021intro ha
  22. 0022intro hd
  23. 0023have hhsh : Lt(h,sh)
    Exact native replay linehave hhsh : exists gap. gap + S h = sh
  24. 0024rewrite hsh
  25. 0025specialize le_refl (S h)
  26. 0026exact le_refl
  27. 0027have hsplit_stored : ∃ n. ∃ r. ∃ storeda. BetaAt(bb,bc,j,n) ∧ BetaAt(db,dc,j,r) ∧ BetaAt(tb,tc,j,storeda) ∧ (∃ x. ∃ y. (∀ z. Lt(z,sh) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(p · S j,q · S z) ∧ ¬Lt(q · S z,p · S j)) ∨ m = 1 ∧ (Lt(q · S z,p · S j) ∧ ¬Lt(p · S j,q · S z)))) ∧ BitCount(x,y,sh,n) ∧ ((∀ z. Lt(z,h) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(p · S j,q · S z) ∧ ¬Lt(q · S z,p · S j)) ∨ m = 1 ∧ (Lt(q · S z,p · S j) ∧ ¬Lt(p · S j,q · S z)))) ∧ BetaAt(x,y,h,storeda)) ∧ (BitCount(x,y,h,r) ∧ (storeda = 0 ∨ storeda = 1) ∧ n = r + storeda))
    Exact native replay linehave hsplit_stored : exists n r storeda. (((((((exists ff_h_efrd_fubini_terminal_column_split_stored_outer_entry. ff_h_efrd_fubini_terminal_column_split_stored_outer_entry + S (n) = S ((S (j)) * bc)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_outer_entry. bb = ff_q_efrd_fubini_terminal_column_split_stored_outer_entry * S ((S (j)) * bc) + (n))) /\ (((exists ff_h_efrd_fubini_terminal_column_split_stored_reduced_entry. ff_h_efrd_fubini_terminal_column_split_stored_reduced_entry + S (r) = S ((S (j)) * dc)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_reduced_entry. db = ff_q_efrd_fubini_terminal_column_split_stored_reduced_entry * S ((S (j)) * dc) + (r)))) /\ (((exists ff_h_efrd_fubini_terminal_column_split_stored_terminal_entry. ff_h_efrd_fubini_terminal_column_split_stored_terminal_entry + S (storeda) = S ((S (j)) * tc)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_terminal_entry. tb = ff_q_efrd_fubini_terminal_column_split_stored_terminal_entry * S ((S (j)) * tc) + (storeda)))) /\ (exists efrd_row_code_fubini_terminal_column_split_stored_split efrd_row_scale_fubini_terminal_column_split_stored_split. (((((forall eri_column_efrd_fubini_terminal_column_split_stored_split_successor_prefix. (exists eri_gap_efrd_fubini_terminal_column_split_stored_split_successor_prefix_bound. eri_gap_efrd_fubini_terminal_column_split_stored_split_successor_prefix_bound + S (eri_column_efrd_fubini_terminal_column_split_stored_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_terminal_column_split_stored_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_terminal_column_split_stored_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_terminal_column_split_stored_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_terminal_column_split_stored_split_successor_prefix) = S ((S (eri_column_efrd_fubini_terminal_column_split_stored_split_successor_prefix)) * efrd_row_scale_fubini_terminal_column_split_stored_split)) /\ exists ff_q_eri_efrd_fubini_terminal_column_split_stored_split_successor_prefix_decoded. efrd_row_code_fubini_terminal_column_split_stored_split = ff_q_eri_efrd_fubini_terminal_column_split_stored_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_terminal_column_split_stored_split_successor_prefix)) * efrd_row_scale_fubini_terminal_column_split_stored_split) + (eri_bit_efrd_fubini_terminal_column_split_stored_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_terminal_column_split_stored_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_terminal_column_split_stored_split_successor_prefix_choice_left. eri_gap_efrd_fubini_terminal_column_split_stored_split_successor_prefix_choice_left + S (p * S j) = q * S eri_column_efrd_fubini_terminal_column_split_stored_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_terminal_column_split_stored_split_successor_prefix_choice_right. eri_gap_efrd_fubini_terminal_column_split_stored_split_successor_prefix_choice_right + S (q * S eri_column_efrd_fubini_terminal_column_split_stored_split_successor_prefix) = p * S j))) \/ (eri_bit_efrd_fubini_terminal_column_split_stored_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_terminal_column_split_stored_split_successor_prefix_choice_right. eri_gap_efrd_fubini_terminal_column_split_stored_split_successor_prefix_choice_right + S (q * S eri_column_efrd_fubini_terminal_column_split_stored_split_successor_prefix) = p * S j) /\ ~(exists eri_gap_efrd_fubini_terminal_column_split_stored_split_successor_prefix_choice_left. eri_gap_efrd_fubini_terminal_column_split_stored_split_successor_prefix_choice_left + S (p * S j) = q * S eri_column_efrd_fubini_terminal_column_split_stored_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_terminal_column_split_stored_split_successor_count_sum ff_v_efrd_fubini_terminal_column_split_stored_split_successor_count_sum. ((((exists ff_h_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_start. ff_h_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_terminal_column_split_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_start. ff_u_efrd_fubini_terminal_column_split_stored_split_successor_count_sum = ff_q_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_terminal_column_split_stored_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_terminal. ff_h_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_terminal + S (n) = S ((S (sh)) * ff_v_efrd_fubini_terminal_column_split_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_terminal. ff_u_efrd_fubini_terminal_column_split_stored_split_successor_count_sum = ff_q_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_terminal_column_split_stored_split_successor_count_sum) + (n))) /\ forall ff_i_efrd_fubini_terminal_column_split_stored_split_successor_count_sum. (exists ff_lt_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_bound. ff_lt_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_bound + S ff_i_efrd_fubini_terminal_column_split_stored_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_terminal_column_split_stored_split_successor_count_sum ff_r_efrd_fubini_terminal_column_split_stored_split_successor_count_sum ff_s_efrd_fubini_terminal_column_split_stored_split_successor_count_sum. ((((exists ff_h_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_summand. ff_h_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_summand + S (ff_a_efrd_fubini_terminal_column_split_stored_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_terminal_column_split_stored_split_successor_count_sum)) * efrd_row_scale_fubini_terminal_column_split_stored_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_summand. efrd_row_code_fubini_terminal_column_split_stored_split = ff_q_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_terminal_column_split_stored_split_successor_count_sum)) * efrd_row_scale_fubini_terminal_column_split_stored_split) + (ff_a_efrd_fubini_terminal_column_split_stored_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_partial. ff_h_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_partial + S (ff_r_efrd_fubini_terminal_column_split_stored_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_terminal_column_split_stored_split_successor_count_sum)) * ff_v_efrd_fubini_terminal_column_split_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_partial. ff_u_efrd_fubini_terminal_column_split_stored_split_successor_count_sum = ff_q_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_terminal_column_split_stored_split_successor_count_sum)) * ff_v_efrd_fubini_terminal_column_split_stored_split_successor_count_sum) + (ff_r_efrd_fubini_terminal_column_split_stored_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_successor. ff_h_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_successor + S (ff_s_efrd_fubini_terminal_column_split_stored_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_terminal_column_split_stored_split_successor_count_sum)) * ff_v_efrd_fubini_terminal_column_split_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_successor. ff_u_efrd_fubini_terminal_column_split_stored_split_successor_count_sum = ff_q_efrd_fubini_terminal_column_split_stored_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_terminal_column_split_stored_split_successor_count_sum)) * ff_v_efrd_fubini_terminal_column_split_stored_split_successor_count_sum) + (ff_s_efrd_fubini_terminal_column_split_stored_split_successor_count_sum))) /\ ff_s_efrd_fubini_terminal_column_split_stored_split_successor_count_sum = ff_r_efrd_fubini_terminal_column_split_stored_split_successor_count_sum + ff_a_efrd_fubini_terminal_column_split_stored_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_terminal_column_split_stored_split_successor_count_bits. (exists ff_lt_efrd_fubini_terminal_column_split_stored_split_successor_count_bits_bound. ff_lt_efrd_fubini_terminal_column_split_stored_split_successor_count_bits_bound + S ff_i_efrd_fubini_terminal_column_split_stored_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_terminal_column_split_stored_split_successor_count_bits. ((((exists ff_h_efrd_fubini_terminal_column_split_stored_split_successor_count_bits_decoded. ff_h_efrd_fubini_terminal_column_split_stored_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_terminal_column_split_stored_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_terminal_column_split_stored_split_successor_count_bits)) * efrd_row_scale_fubini_terminal_column_split_stored_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_split_successor_count_bits_decoded. efrd_row_code_fubini_terminal_column_split_stored_split = ff_q_efrd_fubini_terminal_column_split_stored_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_terminal_column_split_stored_split_successor_count_bits)) * efrd_row_scale_fubini_terminal_column_split_stored_split) + (ff_bit_efrd_fubini_terminal_column_split_stored_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_terminal_column_split_stored_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_terminal_column_split_stored_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_terminal_column_split_stored_split_reduced_prefix. (exists eri_gap_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_bound. eri_gap_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_bound + S (eri_column_efrd_fubini_terminal_column_split_stored_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_terminal_column_split_stored_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_terminal_column_split_stored_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_terminal_column_split_stored_split_reduced_prefix)) * efrd_row_scale_fubini_terminal_column_split_stored_split)) /\ exists ff_q_eri_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_decoded. efrd_row_code_fubini_terminal_column_split_stored_split = ff_q_eri_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_terminal_column_split_stored_split_reduced_prefix)) * efrd_row_scale_fubini_terminal_column_split_stored_split) + (eri_bit_efrd_fubini_terminal_column_split_stored_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_terminal_column_split_stored_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_choice_left + S (p * S j) = q * S eri_column_efrd_fubini_terminal_column_split_stored_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_choice_right + S (q * S eri_column_efrd_fubini_terminal_column_split_stored_split_reduced_prefix) = p * S j))) \/ (eri_bit_efrd_fubini_terminal_column_split_stored_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_choice_right + S (q * S eri_column_efrd_fubini_terminal_column_split_stored_split_reduced_prefix) = p * S j) /\ ~(exists eri_gap_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_terminal_column_split_stored_split_reduced_prefix_choice_left + S (p * S j) = q * S eri_column_efrd_fubini_terminal_column_split_stored_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_terminal_column_split_stored_split_terminal_entry. ff_h_efrd_fubini_terminal_column_split_stored_split_terminal_entry + S (storeda) = S ((S (h)) * efrd_row_scale_fubini_terminal_column_split_stored_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_split_terminal_entry. efrd_row_code_fubini_terminal_column_split_stored_split = ff_q_efrd_fubini_terminal_column_split_stored_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_terminal_column_split_stored_split) + (storeda))))) /\ (((((exists ff_u_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum ff_v_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_start. ff_h_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_start. ff_u_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum = ff_q_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_terminal. ff_h_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_terminal + S (r) = S ((S (h)) * ff_v_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_terminal. ff_u_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum = ff_q_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum) + (r))) /\ forall ff_i_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum. (exists ff_lt_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_bound. ff_lt_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_bound + S ff_i_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum ff_r_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum ff_s_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_summand. ff_h_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum)) * efrd_row_scale_fubini_terminal_column_split_stored_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_summand. efrd_row_code_fubini_terminal_column_split_stored_split = ff_q_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum)) * efrd_row_scale_fubini_terminal_column_split_stored_split) + (ff_a_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_partial. ff_h_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_partial. ff_u_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum = ff_q_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum) + (ff_r_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_successor. ff_h_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_successor. ff_u_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum = ff_q_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum) + (ff_s_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum))) /\ ff_s_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum = ff_r_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum + ff_a_efrd_fubini_terminal_column_split_stored_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits. (exists ff_lt_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits_bound. ff_lt_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits_bound + S ff_i_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits_decoded. ff_h_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits)) * efrd_row_scale_fubini_terminal_column_split_stored_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits_decoded. efrd_row_code_fubini_terminal_column_split_stored_split = ff_q_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits)) * efrd_row_scale_fubini_terminal_column_split_stored_split) + (ff_bit_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_terminal_column_split_stored_split_reduced_count_bits = 1))))) /\ (storeda = 0 \/ storeda = 1)) /\ n = r + storeda))))))
  28. 0028specialize hsplit j
  29. 0029apply hsplit
  30. 0030exact hj
  31. 0031cases hsplit_stored
  32. 0032cases hsplit_stored_witness
  33. 0033cases hsplit_stored_witness_witness
  34. 0034cases hsplit_stored_witness_witness_witness
  35. 0035cases hsplit_stored_witness_witness_witness_left
  36. 0036cases hsplit_stored_witness_witness_witness_left_left
  37. 0037have hstored_a_eq : x2 = a
  38. 0038specialize beta_at_unique tb
  39. 0039specialize beta_at_unique tc
  40. 0040specialize beta_at_unique j
  41. 0041specialize beta_at_unique x2
  42. 0042specialize beta_at_unique a
  43. 0043apply beta_at_unique
  44. 0044exact hsplit_stored_witness_witness_witness_left_right
  45. 0045exact ha
  46. 0046cases hsplit_stored_witness_witness_witness_right
  47. 0047cases hsplit_stored_witness_witness_witness_right_witness
  48. 0048cases hsplit_stored_witness_witness_witness_right_witness_witness
  49. 0049cases hsplit_stored_witness_witness_witness_right_witness_witness_left
  50. 0050cases hsplit_stored_witness_witness_witness_right_witness_witness_left_left
  51. 0051cases hsplit_stored_witness_witness_witness_right_witness_witness_left_right
  52. 0052have hterminal_choice : x2 = 0 ∧ (Lt(p · S j,q · S h) ∧ ¬Lt(q · S h,p · S j)) ∨ x2 = 1 ∧ (Lt(q · S h,p · S j) ∧ ¬Lt(p · S j,q · S h))
    Exact native replay linehave hterminal_choice : ((x2 = 0 /\ ((exists eri_gap_fubini_terminal_column_terminal_choice_left. eri_gap_fubini_terminal_column_terminal_choice_left + S (p * S j) = q * S h) /\ ~(exists eri_gap_fubini_terminal_column_terminal_choice_right. eri_gap_fubini_terminal_column_terminal_choice_right + S (q * S h) = p * S j))) \/ (x2 = 1 /\ ((exists eri_gap_fubini_terminal_column_terminal_choice_right. eri_gap_fubini_terminal_column_terminal_choice_right + S (q * S h) = p * S j) /\ ~(exists eri_gap_fubini_terminal_column_terminal_choice_left. eri_gap_fubini_terminal_column_terminal_choice_left + S (p * S j) = q * S h))))
  53. 0053specialize eisenstein_row_indicator_decoded_choice q
  54. 0054specialize eisenstein_row_indicator_decoded_choice p
  55. 0055specialize eisenstein_row_indicator_decoded_choice j
  56. 0056specialize eisenstein_row_indicator_decoded_choice x3
  57. 0057specialize eisenstein_row_indicator_decoded_choice x4
  58. 0058specialize eisenstein_row_indicator_decoded_choice sh
  59. 0059specialize eisenstein_row_indicator_decoded_choice h
  60. 0060specialize eisenstein_row_indicator_decoded_choice x2
  61. 0061apply eisenstein_row_indicator_decoded_choice
  62. 0062exact hsplit_stored_witness_witness_witness_right_witness_witness_left_left_left
  63. 0063exact hhsh
  64. 0064exact hsplit_stored_witness_witness_witness_right_witness_witness_left_right_right
  65. 0065have hcolumn_stored : ∃ storedd. BetaAt(cb,cc,j,storedd) ∧ (∃ x. ∃ y. ∃ z. BetaAt(bb,bc,j,x) ∧ (∀ n. Lt(n,sh) → ∃ m. BetaAt(y,z,n,m) ∧ (m = 0 ∧ (Lt(p · S j,q · S n) ∧ ¬Lt(q · S n,p · S j)) ∨ m = 1 ∧ (Lt(q · S n,p · S j) ∧ ¬Lt(p · S j,q · S n)))) ∧ BitCount(y,z,sh,x) ∧ BetaAt(y,z,h,storedd))
    Exact native replay linehave hcolumn_stored : exists storedd. ((((exists ff_h_fubini_terminal_column_stored_entry. ff_h_fubini_terminal_column_stored_entry + S (storedd) = S ((S (j)) * cc)) /\ exists ff_q_fubini_terminal_column_stored_entry. cb = ff_q_fubini_terminal_column_stored_entry * S ((S (j)) * cc) + (storedd))) /\ (exists etc_count_fubini_terminal_column_stored_witness etc_row_code_fubini_terminal_column_stored_witness etc_row_scale_fubini_terminal_column_stored_witness. ((((((exists ff_h_etc_fubini_terminal_column_stored_witness_outer_entry. ff_h_etc_fubini_terminal_column_stored_witness_outer_entry + S (etc_count_fubini_terminal_column_stored_witness) = S ((S (j)) * bc)) /\ exists ff_q_etc_fubini_terminal_column_stored_witness_outer_entry. bb = ff_q_etc_fubini_terminal_column_stored_witness_outer_entry * S ((S (j)) * bc) + (etc_count_fubini_terminal_column_stored_witness))) /\ (forall eri_column_etc_fubini_terminal_column_stored_witness_row. (exists eri_gap_etc_fubini_terminal_column_stored_witness_row_bound. eri_gap_etc_fubini_terminal_column_stored_witness_row_bound + S (eri_column_etc_fubini_terminal_column_stored_witness_row) = sh) -> exists eri_bit_etc_fubini_terminal_column_stored_witness_row. ((((exists ff_h_eri_etc_fubini_terminal_column_stored_witness_row_decoded. ff_h_eri_etc_fubini_terminal_column_stored_witness_row_decoded + S (eri_bit_etc_fubini_terminal_column_stored_witness_row) = S ((S (eri_column_etc_fubini_terminal_column_stored_witness_row)) * etc_row_scale_fubini_terminal_column_stored_witness)) /\ exists ff_q_eri_etc_fubini_terminal_column_stored_witness_row_decoded. etc_row_code_fubini_terminal_column_stored_witness = ff_q_eri_etc_fubini_terminal_column_stored_witness_row_decoded * S ((S (eri_column_etc_fubini_terminal_column_stored_witness_row)) * etc_row_scale_fubini_terminal_column_stored_witness) + (eri_bit_etc_fubini_terminal_column_stored_witness_row))) /\ (((eri_bit_etc_fubini_terminal_column_stored_witness_row = 0 /\ ((exists eri_gap_etc_fubini_terminal_column_stored_witness_row_choice_left. eri_gap_etc_fubini_terminal_column_stored_witness_row_choice_left + S (p * S j) = q * S eri_column_etc_fubini_terminal_column_stored_witness_row) /\ ~(exists eri_gap_etc_fubini_terminal_column_stored_witness_row_choice_right. eri_gap_etc_fubini_terminal_column_stored_witness_row_choice_right + S (q * S eri_column_etc_fubini_terminal_column_stored_witness_row) = p * S j))) \/ (eri_bit_etc_fubini_terminal_column_stored_witness_row = 1 /\ ((exists eri_gap_etc_fubini_terminal_column_stored_witness_row_choice_right. eri_gap_etc_fubini_terminal_column_stored_witness_row_choice_right + S (q * S eri_column_etc_fubini_terminal_column_stored_witness_row) = p * S j) /\ ~(exists eri_gap_etc_fubini_terminal_column_stored_witness_row_choice_left. eri_gap_etc_fubini_terminal_column_stored_witness_row_choice_left + S (p * S j) = q * S eri_column_etc_fubini_terminal_column_stored_witness_row)))))))) /\ (((exists ff_u_etc_fubini_terminal_column_stored_witness_count_relation_sum ff_v_etc_fubini_terminal_column_stored_witness_count_relation_sum. ((((exists ff_h_etc_fubini_terminal_column_stored_witness_count_relation_sum_start. ff_h_etc_fubini_terminal_column_stored_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_fubini_terminal_column_stored_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_terminal_column_stored_witness_count_relation_sum_start. ff_u_etc_fubini_terminal_column_stored_witness_count_relation_sum = ff_q_etc_fubini_terminal_column_stored_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_fubini_terminal_column_stored_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_fubini_terminal_column_stored_witness_count_relation_sum_terminal. ff_h_etc_fubini_terminal_column_stored_witness_count_relation_sum_terminal + S (etc_count_fubini_terminal_column_stored_witness) = S ((S (sh)) * ff_v_etc_fubini_terminal_column_stored_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_terminal_column_stored_witness_count_relation_sum_terminal. ff_u_etc_fubini_terminal_column_stored_witness_count_relation_sum = ff_q_etc_fubini_terminal_column_stored_witness_count_relation_sum_terminal * S ((S (sh)) * ff_v_etc_fubini_terminal_column_stored_witness_count_relation_sum) + (etc_count_fubini_terminal_column_stored_witness))) /\ forall ff_i_etc_fubini_terminal_column_stored_witness_count_relation_sum. (exists ff_lt_etc_fubini_terminal_column_stored_witness_count_relation_sum_bound. ff_lt_etc_fubini_terminal_column_stored_witness_count_relation_sum_bound + S ff_i_etc_fubini_terminal_column_stored_witness_count_relation_sum = sh) -> exists ff_a_etc_fubini_terminal_column_stored_witness_count_relation_sum ff_r_etc_fubini_terminal_column_stored_witness_count_relation_sum ff_s_etc_fubini_terminal_column_stored_witness_count_relation_sum. ((((exists ff_h_etc_fubini_terminal_column_stored_witness_count_relation_sum_summand. ff_h_etc_fubini_terminal_column_stored_witness_count_relation_sum_summand + S (ff_a_etc_fubini_terminal_column_stored_witness_count_relation_sum) = S ((S (ff_i_etc_fubini_terminal_column_stored_witness_count_relation_sum)) * etc_row_scale_fubini_terminal_column_stored_witness)) /\ exists ff_q_etc_fubini_terminal_column_stored_witness_count_relation_sum_summand. etc_row_code_fubini_terminal_column_stored_witness = ff_q_etc_fubini_terminal_column_stored_witness_count_relation_sum_summand * S ((S (ff_i_etc_fubini_terminal_column_stored_witness_count_relation_sum)) * etc_row_scale_fubini_terminal_column_stored_witness) + (ff_a_etc_fubini_terminal_column_stored_witness_count_relation_sum))) /\ ((((exists ff_h_etc_fubini_terminal_column_stored_witness_count_relation_sum_partial. ff_h_etc_fubini_terminal_column_stored_witness_count_relation_sum_partial + S (ff_r_etc_fubini_terminal_column_stored_witness_count_relation_sum) = S ((S (ff_i_etc_fubini_terminal_column_stored_witness_count_relation_sum)) * ff_v_etc_fubini_terminal_column_stored_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_terminal_column_stored_witness_count_relation_sum_partial. ff_u_etc_fubini_terminal_column_stored_witness_count_relation_sum = ff_q_etc_fubini_terminal_column_stored_witness_count_relation_sum_partial * S ((S (ff_i_etc_fubini_terminal_column_stored_witness_count_relation_sum)) * ff_v_etc_fubini_terminal_column_stored_witness_count_relation_sum) + (ff_r_etc_fubini_terminal_column_stored_witness_count_relation_sum))) /\ ((((exists ff_h_etc_fubini_terminal_column_stored_witness_count_relation_sum_successor. ff_h_etc_fubini_terminal_column_stored_witness_count_relation_sum_successor + S (ff_s_etc_fubini_terminal_column_stored_witness_count_relation_sum) = S ((S (S ff_i_etc_fubini_terminal_column_stored_witness_count_relation_sum)) * ff_v_etc_fubini_terminal_column_stored_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_terminal_column_stored_witness_count_relation_sum_successor. ff_u_etc_fubini_terminal_column_stored_witness_count_relation_sum = ff_q_etc_fubini_terminal_column_stored_witness_count_relation_sum_successor * S ((S (S ff_i_etc_fubini_terminal_column_stored_witness_count_relation_sum)) * ff_v_etc_fubini_terminal_column_stored_witness_count_relation_sum) + (ff_s_etc_fubini_terminal_column_stored_witness_count_relation_sum))) /\ ff_s_etc_fubini_terminal_column_stored_witness_count_relation_sum = ff_r_etc_fubini_terminal_column_stored_witness_count_relation_sum + ff_a_etc_fubini_terminal_column_stored_witness_count_relation_sum)))))) /\ (forall ff_i_etc_fubini_terminal_column_stored_witness_count_relation_bits. (exists ff_lt_etc_fubini_terminal_column_stored_witness_count_relation_bits_bound. ff_lt_etc_fubini_terminal_column_stored_witness_count_relation_bits_bound + S ff_i_etc_fubini_terminal_column_stored_witness_count_relation_bits = sh) -> exists ff_bit_etc_fubini_terminal_column_stored_witness_count_relation_bits. ((((exists ff_h_etc_fubini_terminal_column_stored_witness_count_relation_bits_decoded. ff_h_etc_fubini_terminal_column_stored_witness_count_relation_bits_decoded + S (ff_bit_etc_fubini_terminal_column_stored_witness_count_relation_bits) = S ((S (ff_i_etc_fubini_terminal_column_stored_witness_count_relation_bits)) * etc_row_scale_fubini_terminal_column_stored_witness)) /\ exists ff_q_etc_fubini_terminal_column_stored_witness_count_relation_bits_decoded. etc_row_code_fubini_terminal_column_stored_witness = ff_q_etc_fubini_terminal_column_stored_witness_count_relation_bits_decoded * S ((S (ff_i_etc_fubini_terminal_column_stored_witness_count_relation_bits)) * etc_row_scale_fubini_terminal_column_stored_witness) + (ff_bit_etc_fubini_terminal_column_stored_witness_count_relation_bits))) /\ (ff_bit_etc_fubini_terminal_column_stored_witness_count_relation_bits = 0 \/ ff_bit_etc_fubini_terminal_column_stored_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_fubini_terminal_column_stored_witness_inner_entry. ff_h_etc_fubini_terminal_column_stored_witness_inner_entry + S (storedd) = S ((S (h)) * etc_row_scale_fubini_terminal_column_stored_witness)) /\ exists ff_q_etc_fubini_terminal_column_stored_witness_inner_entry. etc_row_code_fubini_terminal_column_stored_witness = ff_q_etc_fubini_terminal_column_stored_witness_inner_entry * S ((S (h)) * etc_row_scale_fubini_terminal_column_stored_witness) + (storedd))))))
  66. 0066specialize hcolumn j
  67. 0067apply hcolumn
  68. 0068exact hj
  69. 0069cases hcolumn_stored
  70. 0070cases hcolumn_stored_witness
  71. 0071have hstored_d_eq : x5 = d
  72. 0072specialize beta_at_unique cb
  73. 0073specialize beta_at_unique cc
  74. 0074specialize beta_at_unique j
  75. 0075specialize beta_at_unique x5
  76. 0076specialize beta_at_unique d
  77. 0077apply beta_at_unique
  78. 0078exact hcolumn_stored_witness_left
  79. 0079exact hd
  80. 0080cases hcolumn_stored_witness_right
  81. 0081cases hcolumn_stored_witness_right_witness
  82. 0082cases hcolumn_stored_witness_right_witness_witness
  83. 0083cases hcolumn_stored_witness_right_witness_witness_witness
  84. 0084cases hcolumn_stored_witness_right_witness_witness_witness_left
  85. 0085cases hcolumn_stored_witness_right_witness_witness_witness_left_left
  86. 0086have hcolumn_choice : x5 = 0 ∧ (Lt(p · S j,q · S h) ∧ ¬Lt(q · S h,p · S j)) ∨ x5 = 1 ∧ (Lt(q · S h,p · S j) ∧ ¬Lt(p · S j,q · S h))
    Exact native replay linehave hcolumn_choice : ((x5 = 0 /\ ((exists eri_gap_fubini_terminal_column_column_choice_left. eri_gap_fubini_terminal_column_column_choice_left + S (p * S j) = q * S h) /\ ~(exists eri_gap_fubini_terminal_column_column_choice_right. eri_gap_fubini_terminal_column_column_choice_right + S (q * S h) = p * S j))) \/ (x5 = 1 /\ ((exists eri_gap_fubini_terminal_column_column_choice_right. eri_gap_fubini_terminal_column_column_choice_right + S (q * S h) = p * S j) /\ ~(exists eri_gap_fubini_terminal_column_column_choice_left. eri_gap_fubini_terminal_column_column_choice_left + S (p * S j) = q * S h))))
  87. 0087specialize eisenstein_row_indicator_decoded_choice q
  88. 0088specialize eisenstein_row_indicator_decoded_choice p
  89. 0089specialize eisenstein_row_indicator_decoded_choice j
  90. 0090specialize eisenstein_row_indicator_decoded_choice x7
  91. 0091specialize eisenstein_row_indicator_decoded_choice x8
  92. 0092specialize eisenstein_row_indicator_decoded_choice sh
  93. 0093specialize eisenstein_row_indicator_decoded_choice h
  94. 0094specialize eisenstein_row_indicator_decoded_choice x5
  95. 0095apply eisenstein_row_indicator_decoded_choice
  96. 0096exact hcolumn_stored_witness_right_witness_witness_witness_left_left_right
  97. 0097exact hhsh
  98. 0098exact hcolumn_stored_witness_right_witness_witness_witness_right
  99. 0099rewrite hstored_a_eq at hterminal_choice
  100. 0100rewrite hstored_a_eq at hterminal_choice
  101. 0101rewrite hstored_d_eq at hcolumn_choice
  102. 0102rewrite hstored_d_eq at hcolumn_choice
  103. 0103specialize eisenstein_cell_indicator_choice_unique q
  104. 0104specialize eisenstein_cell_indicator_choice_unique p
  105. 0105specialize eisenstein_cell_indicator_choice_unique j
  106. 0106specialize eisenstein_cell_indicator_choice_unique h
  107. 0107specialize eisenstein_cell_indicator_choice_unique a
  108. 0108specialize eisenstein_cell_indicator_choice_unique d
  109. 0109apply eisenstein_cell_indicator_choice_unique
  110. 0110exact hterminal_choice
  111. 0111exact hcolumn_choice