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
∀ h. ∀ p. ∀ q. ∀ k. ∀ bb. ∀ bc. ∀ db. ∀ dc. ∀ T. ∀ M. (∀ x. Lt(x,k) → ∃ y. BetaAt(bb,bc,x,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,h) → ∃ i. BetaAt(z,n,m,i) ∧ (i = 0 ∧ (Lt(p · S x,q · S m) ∧ ¬Lt(q · S m,p · S x)) ∨ i = 1 ∧ (Lt(q · S m,p · S x) ∧ ¬Lt(p · S x,q · S m)))) ∧ BitCount(z,n,h,y))) → (∀ x. Lt(x,h) → ∃ y. BetaAt(db,dc,x,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,k) → ∃ i. BetaAt(z,n,m,i) ∧ (∃ j. ∃ u. ∃ v. BetaAt(bb,bc,m,j) ∧ (∀ w. Lt(w,h) → ∃ x0. BetaAt(u,v,w,x0) ∧ (x0 = 0 ∧ (Lt(p · S m,q · S w) ∧ ¬Lt(q · S w,p · S m)) ∨ x0 = 1 ∧ (Lt(q · S w,p · S m) ∧ ¬Lt(p · S m,q · S w)))) ∧ BitCount(u,v,h,j) ∧ BetaAt(u,v,x,i))) ∧ BitCount(z,n,k,y))) → Sum(bb,bc,k,T) → Sum(db,dc,h,M) → M = TEvery 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
25 occurrences
In local proof propositions
73 occurrences
Exact expanded native-PA statement
forall h p q k bb bc db dc T M. (forall erc_row_fubini_total_general_outer. (exists erc_lt_gap_fubini_total_general_outer_bound. erc_lt_gap_fubini_total_general_outer_bound + S (erc_row_fubini_total_general_outer) = k) -> exists erc_count_fubini_total_general_outer. ((((exists ff_h_erc_fubini_total_general_outer_decoded. ff_h_erc_fubini_total_general_outer_decoded + S (erc_count_fubini_total_general_outer) = S ((S (erc_row_fubini_total_general_outer)) * bc)) /\ exists ff_q_erc_fubini_total_general_outer_decoded. bb = ff_q_erc_fubini_total_general_outer_decoded * S ((S (erc_row_fubini_total_general_outer)) * bc) + (erc_count_fubini_total_general_outer))) /\ (exists erc_row_code_fubini_total_general_outer_witness erc_row_scale_fubini_total_general_outer_witness. ((forall eri_column_erc_fubini_total_general_outer_witness_row. (exists eri_gap_erc_fubini_total_general_outer_witness_row_bound. eri_gap_erc_fubini_total_general_outer_witness_row_bound + S (eri_column_erc_fubini_total_general_outer_witness_row) = h) -> exists eri_bit_erc_fubini_total_general_outer_witness_row. ((((exists ff_h_eri_erc_fubini_total_general_outer_witness_row_decoded. ff_h_eri_erc_fubini_total_general_outer_witness_row_decoded + S (eri_bit_erc_fubini_total_general_outer_witness_row) = S ((S (eri_column_erc_fubini_total_general_outer_witness_row)) * erc_row_scale_fubini_total_general_outer_witness)) /\ exists ff_q_eri_erc_fubini_total_general_outer_witness_row_decoded. erc_row_code_fubini_total_general_outer_witness = ff_q_eri_erc_fubini_total_general_outer_witness_row_decoded * S ((S (eri_column_erc_fubini_total_general_outer_witness_row)) * erc_row_scale_fubini_total_general_outer_witness) + (eri_bit_erc_fubini_total_general_outer_witness_row))) /\ (((eri_bit_erc_fubini_total_general_outer_witness_row = 0 /\ ((exists eri_gap_erc_fubini_total_general_outer_witness_row_choice_left. eri_gap_erc_fubini_total_general_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_general_outer) = q * S eri_column_erc_fubini_total_general_outer_witness_row) /\ ~(exists eri_gap_erc_fubini_total_general_outer_witness_row_choice_right. eri_gap_erc_fubini_total_general_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_general_outer_witness_row) = p * S erc_row_fubini_total_general_outer))) \/ (eri_bit_erc_fubini_total_general_outer_witness_row = 1 /\ ((exists eri_gap_erc_fubini_total_general_outer_witness_row_choice_right. eri_gap_erc_fubini_total_general_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_general_outer_witness_row) = p * S erc_row_fubini_total_general_outer) /\ ~(exists eri_gap_erc_fubini_total_general_outer_witness_row_choice_left. eri_gap_erc_fubini_total_general_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_general_outer) = q * S eri_column_erc_fubini_total_general_outer_witness_row))))))) /\ (((exists ff_u_erc_fubini_total_general_outer_witness_count_sum ff_v_erc_fubini_total_general_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_general_outer_witness_count_sum_start. ff_h_erc_fubini_total_general_outer_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_total_general_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_general_outer_witness_count_sum_start. ff_u_erc_fubini_total_general_outer_witness_count_sum = ff_q_erc_fubini_total_general_outer_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_total_general_outer_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_total_general_outer_witness_count_sum_terminal. ff_h_erc_fubini_total_general_outer_witness_count_sum_terminal + S (erc_count_fubini_total_general_outer) = S ((S (h)) * ff_v_erc_fubini_total_general_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_general_outer_witness_count_sum_terminal. ff_u_erc_fubini_total_general_outer_witness_count_sum = ff_q_erc_fubini_total_general_outer_witness_count_sum_terminal * S ((S (h)) * ff_v_erc_fubini_total_general_outer_witness_count_sum) + (erc_count_fubini_total_general_outer))) /\ forall ff_i_erc_fubini_total_general_outer_witness_count_sum. (exists ff_lt_erc_fubini_total_general_outer_witness_count_sum_bound. ff_lt_erc_fubini_total_general_outer_witness_count_sum_bound + S ff_i_erc_fubini_total_general_outer_witness_count_sum = h) -> exists ff_a_erc_fubini_total_general_outer_witness_count_sum ff_r_erc_fubini_total_general_outer_witness_count_sum ff_s_erc_fubini_total_general_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_general_outer_witness_count_sum_summand. ff_h_erc_fubini_total_general_outer_witness_count_sum_summand + S (ff_a_erc_fubini_total_general_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_general_outer_witness_count_sum)) * erc_row_scale_fubini_total_general_outer_witness)) /\ exists ff_q_erc_fubini_total_general_outer_witness_count_sum_summand. erc_row_code_fubini_total_general_outer_witness = ff_q_erc_fubini_total_general_outer_witness_count_sum_summand * S ((S (ff_i_erc_fubini_total_general_outer_witness_count_sum)) * erc_row_scale_fubini_total_general_outer_witness) + (ff_a_erc_fubini_total_general_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_general_outer_witness_count_sum_partial. ff_h_erc_fubini_total_general_outer_witness_count_sum_partial + S (ff_r_erc_fubini_total_general_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_general_outer_witness_count_sum)) * ff_v_erc_fubini_total_general_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_general_outer_witness_count_sum_partial. ff_u_erc_fubini_total_general_outer_witness_count_sum = ff_q_erc_fubini_total_general_outer_witness_count_sum_partial * S ((S (ff_i_erc_fubini_total_general_outer_witness_count_sum)) * ff_v_erc_fubini_total_general_outer_witness_count_sum) + (ff_r_erc_fubini_total_general_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_general_outer_witness_count_sum_successor. ff_h_erc_fubini_total_general_outer_witness_count_sum_successor + S (ff_s_erc_fubini_total_general_outer_witness_count_sum) = S ((S (S ff_i_erc_fubini_total_general_outer_witness_count_sum)) * ff_v_erc_fubini_total_general_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_general_outer_witness_count_sum_successor. ff_u_erc_fubini_total_general_outer_witness_count_sum = ff_q_erc_fubini_total_general_outer_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_total_general_outer_witness_count_sum)) * ff_v_erc_fubini_total_general_outer_witness_count_sum) + (ff_s_erc_fubini_total_general_outer_witness_count_sum))) /\ ff_s_erc_fubini_total_general_outer_witness_count_sum = ff_r_erc_fubini_total_general_outer_witness_count_sum + ff_a_erc_fubini_total_general_outer_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_total_general_outer_witness_count_bits. (exists ff_lt_erc_fubini_total_general_outer_witness_count_bits_bound. ff_lt_erc_fubini_total_general_outer_witness_count_bits_bound + S ff_i_erc_fubini_total_general_outer_witness_count_bits = h) -> exists ff_bit_erc_fubini_total_general_outer_witness_count_bits. ((((exists ff_h_erc_fubini_total_general_outer_witness_count_bits_decoded. ff_h_erc_fubini_total_general_outer_witness_count_bits_decoded + S (ff_bit_erc_fubini_total_general_outer_witness_count_bits) = S ((S (ff_i_erc_fubini_total_general_outer_witness_count_bits)) * erc_row_scale_fubini_total_general_outer_witness)) /\ exists ff_q_erc_fubini_total_general_outer_witness_count_bits_decoded. erc_row_code_fubini_total_general_outer_witness = ff_q_erc_fubini_total_general_outer_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_total_general_outer_witness_count_bits)) * erc_row_scale_fubini_total_general_outer_witness) + (ff_bit_erc_fubini_total_general_outer_witness_count_bits))) /\ (ff_bit_erc_fubini_total_general_outer_witness_count_bits = 0 \/ ff_bit_erc_fubini_total_general_outer_witness_count_bits = 1))))))))) -> (forall eft_fixed_index_fubini_total_general_columns. (exists edt_lt_gap_eft_fubini_total_general_columns_bound. edt_lt_gap_eft_fubini_total_general_columns_bound + S (eft_fixed_index_fubini_total_general_columns) = h) -> exists eft_count_fubini_total_general_columns. ((((exists ff_h_eft_fubini_total_general_columns_decoded. ff_h_eft_fubini_total_general_columns_decoded + S (eft_count_fubini_total_general_columns) = S ((S (eft_fixed_index_fubini_total_general_columns)) * dc)) /\ exists ff_q_eft_fubini_total_general_columns_decoded. db = ff_q_eft_fubini_total_general_columns_decoded * S ((S (eft_fixed_index_fubini_total_general_columns)) * dc) + (eft_count_fubini_total_general_columns))) /\ (exists eft_column_code_fubini_total_general_columns_witness eft_column_scale_fubini_total_general_columns_witness. ((forall etc_row_index_eft_fubini_total_general_columns_witness_column. (exists edt_lt_gap_eft_fubini_total_general_columns_witness_column_bound. edt_lt_gap_eft_fubini_total_general_columns_witness_column_bound + S (etc_row_index_eft_fubini_total_general_columns_witness_column) = k) -> exists etc_bit_eft_fubini_total_general_columns_witness_column. ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_decoded. ff_h_etc_eft_fubini_total_general_columns_witness_column_decoded + S (etc_bit_eft_fubini_total_general_columns_witness_column) = S ((S (etc_row_index_eft_fubini_total_general_columns_witness_column)) * eft_column_scale_fubini_total_general_columns_witness)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_decoded. eft_column_code_fubini_total_general_columns_witness = ff_q_etc_eft_fubini_total_general_columns_witness_column_decoded * S ((S (etc_row_index_eft_fubini_total_general_columns_witness_column)) * eft_column_scale_fubini_total_general_columns_witness) + (etc_bit_eft_fubini_total_general_columns_witness_column))) /\ (exists etc_count_eft_fubini_total_general_columns_witness_column_witness etc_row_code_eft_fubini_total_general_columns_witness_column_witness etc_row_scale_eft_fubini_total_general_columns_witness_column_witness. ((((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_outer_entry. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_outer_entry + S (etc_count_eft_fubini_total_general_columns_witness_column_witness) = S ((S (etc_row_index_eft_fubini_total_general_columns_witness_column)) * bc)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_outer_entry. bb = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_outer_entry * S ((S (etc_row_index_eft_fubini_total_general_columns_witness_column)) * bc) + (etc_count_eft_fubini_total_general_columns_witness_column_witness))) /\ (forall eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row. (exists eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_bound. eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_bound + S (eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row) = h) -> exists eri_bit_etc_eft_fubini_total_general_columns_witness_column_witness_row. ((((exists ff_h_eri_etc_eft_fubini_total_general_columns_witness_column_witness_row_decoded. ff_h_eri_etc_eft_fubini_total_general_columns_witness_column_witness_row_decoded + S (eri_bit_etc_eft_fubini_total_general_columns_witness_column_witness_row) = S ((S (eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness)) /\ exists ff_q_eri_etc_eft_fubini_total_general_columns_witness_column_witness_row_decoded. etc_row_code_eft_fubini_total_general_columns_witness_column_witness = ff_q_eri_etc_eft_fubini_total_general_columns_witness_column_witness_row_decoded * S ((S (eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness) + (eri_bit_etc_eft_fubini_total_general_columns_witness_column_witness_row))) /\ (((eri_bit_etc_eft_fubini_total_general_columns_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_general_columns_witness_column) = q * S eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row) /\ ~(exists eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_general_columns_witness_column))) \/ (eri_bit_etc_eft_fubini_total_general_columns_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_general_columns_witness_column) /\ ~(exists eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_general_columns_witness_column) = q * S eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_start. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_start. ff_u_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_terminal. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_terminal + S (etc_count_eft_fubini_total_general_columns_witness_column_witness) = S ((S (h)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_terminal. ff_u_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) + (etc_count_eft_fubini_total_general_columns_witness_column_witness))) /\ forall ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum. (exists ff_lt_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_bound. ff_lt_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_bound + S ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum = h) -> exists ff_a_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum ff_r_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum ff_s_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_summand. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_summand. etc_row_code_eft_fubini_total_general_columns_witness_column_witness = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness) + (ff_a_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_partial. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_partial. ff_u_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) + (ff_r_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_successor. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_successor. ff_u_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) + (ff_s_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum))) /\ ff_s_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum = ff_r_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum + ff_a_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits. (exists ff_lt_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits_bound. ff_lt_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits_bound + S ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits = h) -> exists ff_bit_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits_decoded. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits_decoded. etc_row_code_eft_fubini_total_general_columns_witness_column_witness = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness) + (ff_bit_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_inner_entry. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_inner_entry + S (etc_bit_eft_fubini_total_general_columns_witness_column) = S ((S (eft_fixed_index_fubini_total_general_columns)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_inner_entry. etc_row_code_eft_fubini_total_general_columns_witness_column_witness = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_inner_entry * S ((S (eft_fixed_index_fubini_total_general_columns)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness) + (etc_bit_eft_fubini_total_general_columns_witness_column))))))) /\ (((exists ff_u_eft_fubini_total_general_columns_witness_count_sum ff_v_eft_fubini_total_general_columns_witness_count_sum. ((((exists ff_h_eft_fubini_total_general_columns_witness_count_sum_start. ff_h_eft_fubini_total_general_columns_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_eft_fubini_total_general_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_general_columns_witness_count_sum_start. ff_u_eft_fubini_total_general_columns_witness_count_sum = ff_q_eft_fubini_total_general_columns_witness_count_sum_start * S ((S (0)) * ff_v_eft_fubini_total_general_columns_witness_count_sum) + (0))) /\ ((((exists ff_h_eft_fubini_total_general_columns_witness_count_sum_terminal. ff_h_eft_fubini_total_general_columns_witness_count_sum_terminal + S (eft_count_fubini_total_general_columns) = S ((S (k)) * ff_v_eft_fubini_total_general_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_general_columns_witness_count_sum_terminal. ff_u_eft_fubini_total_general_columns_witness_count_sum = ff_q_eft_fubini_total_general_columns_witness_count_sum_terminal * S ((S (k)) * ff_v_eft_fubini_total_general_columns_witness_count_sum) + (eft_count_fubini_total_general_columns))) /\ forall ff_i_eft_fubini_total_general_columns_witness_count_sum. (exists ff_lt_eft_fubini_total_general_columns_witness_count_sum_bound. ff_lt_eft_fubini_total_general_columns_witness_count_sum_bound + S ff_i_eft_fubini_total_general_columns_witness_count_sum = k) -> exists ff_a_eft_fubini_total_general_columns_witness_count_sum ff_r_eft_fubini_total_general_columns_witness_count_sum ff_s_eft_fubini_total_general_columns_witness_count_sum. ((((exists ff_h_eft_fubini_total_general_columns_witness_count_sum_summand. ff_h_eft_fubini_total_general_columns_witness_count_sum_summand + S (ff_a_eft_fubini_total_general_columns_witness_count_sum) = S ((S (ff_i_eft_fubini_total_general_columns_witness_count_sum)) * eft_column_scale_fubini_total_general_columns_witness)) /\ exists ff_q_eft_fubini_total_general_columns_witness_count_sum_summand. eft_column_code_fubini_total_general_columns_witness = ff_q_eft_fubini_total_general_columns_witness_count_sum_summand * S ((S (ff_i_eft_fubini_total_general_columns_witness_count_sum)) * eft_column_scale_fubini_total_general_columns_witness) + (ff_a_eft_fubini_total_general_columns_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_general_columns_witness_count_sum_partial. ff_h_eft_fubini_total_general_columns_witness_count_sum_partial + S (ff_r_eft_fubini_total_general_columns_witness_count_sum) = S ((S (ff_i_eft_fubini_total_general_columns_witness_count_sum)) * ff_v_eft_fubini_total_general_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_general_columns_witness_count_sum_partial. ff_u_eft_fubini_total_general_columns_witness_count_sum = ff_q_eft_fubini_total_general_columns_witness_count_sum_partial * S ((S (ff_i_eft_fubini_total_general_columns_witness_count_sum)) * ff_v_eft_fubini_total_general_columns_witness_count_sum) + (ff_r_eft_fubini_total_general_columns_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_general_columns_witness_count_sum_successor. ff_h_eft_fubini_total_general_columns_witness_count_sum_successor + S (ff_s_eft_fubini_total_general_columns_witness_count_sum) = S ((S (S ff_i_eft_fubini_total_general_columns_witness_count_sum)) * ff_v_eft_fubini_total_general_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_general_columns_witness_count_sum_successor. ff_u_eft_fubini_total_general_columns_witness_count_sum = ff_q_eft_fubini_total_general_columns_witness_count_sum_successor * S ((S (S ff_i_eft_fubini_total_general_columns_witness_count_sum)) * ff_v_eft_fubini_total_general_columns_witness_count_sum) + (ff_s_eft_fubini_total_general_columns_witness_count_sum))) /\ ff_s_eft_fubini_total_general_columns_witness_count_sum = ff_r_eft_fubini_total_general_columns_witness_count_sum + ff_a_eft_fubini_total_general_columns_witness_count_sum)))))) /\ (forall ff_i_eft_fubini_total_general_columns_witness_count_bits. (exists ff_lt_eft_fubini_total_general_columns_witness_count_bits_bound. ff_lt_eft_fubini_total_general_columns_witness_count_bits_bound + S ff_i_eft_fubini_total_general_columns_witness_count_bits = k) -> exists ff_bit_eft_fubini_total_general_columns_witness_count_bits. ((((exists ff_h_eft_fubini_total_general_columns_witness_count_bits_decoded. ff_h_eft_fubini_total_general_columns_witness_count_bits_decoded + S (ff_bit_eft_fubini_total_general_columns_witness_count_bits) = S ((S (ff_i_eft_fubini_total_general_columns_witness_count_bits)) * eft_column_scale_fubini_total_general_columns_witness)) /\ exists ff_q_eft_fubini_total_general_columns_witness_count_bits_decoded. eft_column_code_fubini_total_general_columns_witness = ff_q_eft_fubini_total_general_columns_witness_count_bits_decoded * S ((S (ff_i_eft_fubini_total_general_columns_witness_count_bits)) * eft_column_scale_fubini_total_general_columns_witness) + (ff_bit_eft_fubini_total_general_columns_witness_count_bits))) /\ (ff_bit_eft_fubini_total_general_columns_witness_count_bits = 0 \/ ff_bit_eft_fubini_total_general_columns_witness_count_bits = 1))))))))) -> (exists ff_u_fubini_total_general_outer_sum ff_v_fubini_total_general_outer_sum. ((((exists ff_h_fubini_total_general_outer_sum_start. ff_h_fubini_total_general_outer_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_general_outer_sum)) /\ exists ff_q_fubini_total_general_outer_sum_start. ff_u_fubini_total_general_outer_sum = ff_q_fubini_total_general_outer_sum_start * S ((S (0)) * ff_v_fubini_total_general_outer_sum) + (0))) /\ ((((exists ff_h_fubini_total_general_outer_sum_terminal. ff_h_fubini_total_general_outer_sum_terminal + S (T) = S ((S (k)) * ff_v_fubini_total_general_outer_sum)) /\ exists ff_q_fubini_total_general_outer_sum_terminal. ff_u_fubini_total_general_outer_sum = ff_q_fubini_total_general_outer_sum_terminal * S ((S (k)) * ff_v_fubini_total_general_outer_sum) + (T))) /\ forall ff_i_fubini_total_general_outer_sum. (exists ff_lt_fubini_total_general_outer_sum_bound. ff_lt_fubini_total_general_outer_sum_bound + S ff_i_fubini_total_general_outer_sum = k) -> exists ff_a_fubini_total_general_outer_sum ff_r_fubini_total_general_outer_sum ff_s_fubini_total_general_outer_sum. ((((exists ff_h_fubini_total_general_outer_sum_summand. ff_h_fubini_total_general_outer_sum_summand + S (ff_a_fubini_total_general_outer_sum) = S ((S (ff_i_fubini_total_general_outer_sum)) * bc)) /\ exists ff_q_fubini_total_general_outer_sum_summand. bb = ff_q_fubini_total_general_outer_sum_summand * S ((S (ff_i_fubini_total_general_outer_sum)) * bc) + (ff_a_fubini_total_general_outer_sum))) /\ ((((exists ff_h_fubini_total_general_outer_sum_partial. ff_h_fubini_total_general_outer_sum_partial + S (ff_r_fubini_total_general_outer_sum) = S ((S (ff_i_fubini_total_general_outer_sum)) * ff_v_fubini_total_general_outer_sum)) /\ exists ff_q_fubini_total_general_outer_sum_partial. ff_u_fubini_total_general_outer_sum = ff_q_fubini_total_general_outer_sum_partial * S ((S (ff_i_fubini_total_general_outer_sum)) * ff_v_fubini_total_general_outer_sum) + (ff_r_fubini_total_general_outer_sum))) /\ ((((exists ff_h_fubini_total_general_outer_sum_successor. ff_h_fubini_total_general_outer_sum_successor + S (ff_s_fubini_total_general_outer_sum) = S ((S (S ff_i_fubini_total_general_outer_sum)) * ff_v_fubini_total_general_outer_sum)) /\ exists ff_q_fubini_total_general_outer_sum_successor. ff_u_fubini_total_general_outer_sum = ff_q_fubini_total_general_outer_sum_successor * S ((S (S ff_i_fubini_total_general_outer_sum)) * ff_v_fubini_total_general_outer_sum) + (ff_s_fubini_total_general_outer_sum))) /\ ff_s_fubini_total_general_outer_sum = ff_r_fubini_total_general_outer_sum + ff_a_fubini_total_general_outer_sum)))))) -> (exists ff_u_fubini_total_general_column_sum ff_v_fubini_total_general_column_sum. ((((exists ff_h_fubini_total_general_column_sum_start. ff_h_fubini_total_general_column_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_general_column_sum)) /\ exists ff_q_fubini_total_general_column_sum_start. ff_u_fubini_total_general_column_sum = ff_q_fubini_total_general_column_sum_start * S ((S (0)) * ff_v_fubini_total_general_column_sum) + (0))) /\ ((((exists ff_h_fubini_total_general_column_sum_terminal. ff_h_fubini_total_general_column_sum_terminal + S (M) = S ((S (h)) * ff_v_fubini_total_general_column_sum)) /\ exists ff_q_fubini_total_general_column_sum_terminal. ff_u_fubini_total_general_column_sum = ff_q_fubini_total_general_column_sum_terminal * S ((S (h)) * ff_v_fubini_total_general_column_sum) + (M))) /\ forall ff_i_fubini_total_general_column_sum. (exists ff_lt_fubini_total_general_column_sum_bound. ff_lt_fubini_total_general_column_sum_bound + S ff_i_fubini_total_general_column_sum = h) -> exists ff_a_fubini_total_general_column_sum ff_r_fubini_total_general_column_sum ff_s_fubini_total_general_column_sum. ((((exists ff_h_fubini_total_general_column_sum_summand. ff_h_fubini_total_general_column_sum_summand + S (ff_a_fubini_total_general_column_sum) = S ((S (ff_i_fubini_total_general_column_sum)) * dc)) /\ exists ff_q_fubini_total_general_column_sum_summand. db = ff_q_fubini_total_general_column_sum_summand * S ((S (ff_i_fubini_total_general_column_sum)) * dc) + (ff_a_fubini_total_general_column_sum))) /\ ((((exists ff_h_fubini_total_general_column_sum_partial. ff_h_fubini_total_general_column_sum_partial + S (ff_r_fubini_total_general_column_sum) = S ((S (ff_i_fubini_total_general_column_sum)) * ff_v_fubini_total_general_column_sum)) /\ exists ff_q_fubini_total_general_column_sum_partial. ff_u_fubini_total_general_column_sum = ff_q_fubini_total_general_column_sum_partial * S ((S (ff_i_fubini_total_general_column_sum)) * ff_v_fubini_total_general_column_sum) + (ff_r_fubini_total_general_column_sum))) /\ ((((exists ff_h_fubini_total_general_column_sum_successor. ff_h_fubini_total_general_column_sum_successor + S (ff_s_fubini_total_general_column_sum) = S ((S (S ff_i_fubini_total_general_column_sum)) * ff_v_fubini_total_general_column_sum)) /\ exists ff_q_fubini_total_general_column_sum_successor. ff_u_fubini_total_general_column_sum = ff_q_fubini_total_general_column_sum_successor * S ((S (S ff_i_fubini_total_general_column_sum)) * ff_v_fubini_total_general_column_sum) + (ff_s_fubini_total_general_column_sum))) /\ ff_s_fubini_total_general_column_sum = ff_r_fubini_total_general_column_sum + ff_a_fubini_total_general_column_sum)))))) -> M = TProof neighborhood
Direct theorem prerequisites
PA0047 beta_sum_zero PA00ES eisenstein_zero_width_rectangle_sum_zero PA00EY eisenstein_successor_rectangle_row_split_prefix_exists PA00F0 eisenstein_successor_row_split_reduced_rectangle_prefix PA003H beta_sum_exists PA00F2 eisenstein_successor_row_split_sum_add PA00F3 eisenstein_fubini_column_count_prefix_succ_restrict PA00F8 eisenstein_fubini_column_count_prefix_retarget_predecessor PA003Y beta_sum_succ_decompose PA001A le_refl PA002F beta_at_unique PA00FB eisenstein_successor_terminal_sum_matches_last_columnDirect theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (12)
beta sum zeroeisenstein zero width rectangle sum zeroeisenstein successor rectangle row split prefix existseisenstein successor row split reduced rectangle prefixbeta sum existseisenstein successor row split sum addeisenstein fubini column count prefix succ restricteisenstein fubini column count prefix retarget predecessorbeta sum succ decomposele reflbeta at uniqueeisenstein successor terminal sum matches last column
01Fix variables and assumptionsL1–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro h
02Induction on hL2–11
03Fix variables and assumptionsL12–15
04Establish hmzeroL16–21
05Establish htzeroL22–31
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein zero width rectangle sum zero.
- L22
have htzero : T = 0 - L23
specialize eisenstein_zero_width_rectangle_sum_zero q - L24
specialize eisenstein_zero_width_rectangle_sum_zero p - L25
specialize eisenstein_zero_width_rectangle_sum_zero 0 - L26
specialize eisenstein_zero_width_rectangle_sum_zero bb - L27
specialize eisenstein_zero_width_rectangle_sum_zero bc - L28
specialize eisenstein_zero_width_rectangle_sum_zero k - L29
specialize eisenstein_zero_width_rectangle_sum_zero T - L30
apply eisenstein_zero_width_rectangle_sum_zero - L31
refl
06Use earlier factsL32–33
07Calculate and transport equalitiesL34–34
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L34
trans 0
08Use earlier factsL35–35
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L35
exact hmzero
09Calculate and transport equalitiesL36–36
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L36
symm
10Use earlier factsL37–37
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L37
exact htzero
11Fix variables and assumptionsL38–47
12Fix variables and assumptionsL48–50
13Establish hsplit_existsL51–60
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein successor rectangle row split prefix exists.
- L51
have hsplit_exists : ∃ rb. ∃ rc. ∃ tb. ∃ tc. ∀ x. Lt(x,k) → ∃ y. ∃ z. ∃ n. BetaAt(bb,bc,x,y) ∧ BetaAt(rb,rc,x,z) ∧ BetaAt(tb,tc,x,n) ∧ (∃ m. ∃ i. (∀ j. Lt(j,S h) → ∃ u. BetaAt(m,i,j,u) ∧ (u = 0 ∧ (Lt(p · S x,q · S j) ∧ ¬Lt(q · S j,p · S x)) ∨ u = 1 ∧ (Lt(q · S j,p · S x) ∧ ¬Lt(p · S x,q · S j)))) ∧ BitCount(m,i,S h,y) ∧ ((∀ j. Lt(j,h) → ∃ u. BetaAt(m,i,j,u) ∧ (u = 0 ∧ (Lt(p · S x,q · S j) ∧ ¬Lt(q · S j,p · S x)) ∨ u = 1 ∧ (Lt(q · S j,p · S x) ∧ ¬Lt(p · S x,q · S j)))) ∧ BetaAt(m,i,h,n)) ∧ (BitCount(m,i,h,z) ∧ (n = 0 ∨ n = 1) ∧ y = z + n))Definitions: Lt(x,k)BetaAt(bb,bc,x,y)BetaAt(rb,rc,x,z)BetaAt(tb,tc,x,n)Lt(j,S h)BetaAt(m,i,j,u)Lt(p · S x,q · S j)Lt(q · S j,p · S x)BitCount(m,i,S h,y)Lt(j,h)BetaAt(m,i,h,n)BitCount(m,i,h,z)Original native command in the exact edition - L52
specialize eisenstein_successor_rectangle_row_split_prefix_exists q - L53
specialize eisenstein_successor_rectangle_row_split_prefix_exists p - L54
specialize eisenstein_successor_rectangle_row_split_prefix_exists h - L55
specialize eisenstein_successor_rectangle_row_split_prefix_exists (S h) - L56
specialize eisenstein_successor_rectangle_row_split_prefix_exists bb - L57
specialize eisenstein_successor_rectangle_row_split_prefix_exists bc - L58
specialize eisenstein_successor_rectangle_row_split_prefix_exists k - L59
apply eisenstein_successor_rectangle_row_split_prefix_exists - L60
refl
14Use earlier factsL61–61
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L61
exact houter
15Separate the logical casesL62–65
16Establish hreduced_outerL66–75
Establish this local claim before using it. It is not an additional assumption.
- L66
have hreduced_outer : ∀ erc_row_fubini_total_universal_reduced_outer. Lt(erc_row_fubini_total_universal_reduced_outer,k) → ∃ y. BetaAt(x,x1,erc_row_fubini_total_universal_reduced_outer,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,h) → ∃ i. BetaAt(z,n,m,i) ∧ (i = 0 ∧ (Lt(p · S erc_row_fubini_total_universal_reduced_outer,q · S m) ∧ ¬Lt(q · S m,p · S erc_row_fubini_total_universal_reduced_outer)) ∨ i = 1 ∧ (Lt(q · S m,p · S erc_row_fubini_total_universal_reduced_outer) ∧ ¬Lt(p · S erc_row_fubini_total_universal_reduced_outer,q · S m)))) ∧ BitCount(z,n,h,y))Definitions: Lt(erc_row_fubini_total_universal_reduced_outer,k)BetaAt(x,x1,erc_row_fubini_total_universal_reduced_outer,y)Lt(m,h)BetaAt(z,n,m,i)Lt(p · S erc_row_fubini_total_universal_reduced_outer,q · S m)Lt(q · S m,p · S erc_row_fubini_total_universal_reduced_outer)BitCount(z,n,h,y)Original native command in the exact edition - L67
specialize eisenstein_successor_row_split_reduced_rectangle_prefix q - L68
specialize eisenstein_successor_row_split_reduced_rectangle_prefix p - L69
specialize eisenstein_successor_row_split_reduced_rectangle_prefix h - L70
specialize eisenstein_successor_row_split_reduced_rectangle_prefix (S h) - L71
specialize eisenstein_successor_row_split_reduced_rectangle_prefix bb - L72
specialize eisenstein_successor_row_split_reduced_rectangle_prefix bc - L73
specialize eisenstein_successor_row_split_reduced_rectangle_prefix x - L74
specialize eisenstein_successor_row_split_reduced_rectangle_prefix x1 - L75
specialize eisenstein_successor_row_split_reduced_rectangle_prefix x2
17Use earlier factsL76–79
Instantiate or apply named facts and discharge the corresponding proof obligations.
18Establish hreduced_sumL80–84
Establish this local claim before using it. It is not an additional assumption.
- L80
have hreduced_sum : ∃ R. Sum(x,x1,k,R)Definitions: Sum(x,x1,k,R)Original native command in the exact edition - L81
specialize beta_sum_exists x - L82
specialize beta_sum_exists x1 - L83
specialize beta_sum_exists k - L84
exact beta_sum_exists
19Separate the logical casesL85–85
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L85
cases hreduced_sum
20Establish hterminal_sumL86–90
Establish this local claim before using it. It is not an additional assumption.
- L86
have hterminal_sum : ∃ D. Sum(x2,x3,k,D)Definitions: Sum(x2,x3,k,D)Original native command in the exact edition - L87
specialize beta_sum_exists x2 - L88
specialize beta_sum_exists x3 - L89
specialize beta_sum_exists k - L90
exact beta_sum_exists
21Separate the logical casesL91–91
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L91
cases hterminal_sum
22Establish hsource_addL92–101
Establish this local claim before using it. It is not an additional assumption.
- L92
have hsource_add : x4 + x5 = T - L93
specialize eisenstein_successor_row_split_sum_add q - L94
specialize eisenstein_successor_row_split_sum_add p - L95
specialize eisenstein_successor_row_split_sum_add h - L96
specialize eisenstein_successor_row_split_sum_add (S h) - L97
specialize eisenstein_successor_row_split_sum_add bb - L98
specialize eisenstein_successor_row_split_sum_add bc - L99
specialize eisenstein_successor_row_split_sum_add x - L100
specialize eisenstein_successor_row_split_sum_add x1 - L101
specialize eisenstein_successor_row_split_sum_add x2
23Use earlier factsL102–111
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L102
specialize eisenstein_successor_row_split_sum_add x3 - L103
specialize eisenstein_successor_row_split_sum_add k - L104
specialize eisenstein_successor_row_split_sum_add x4 - L105
specialize eisenstein_successor_row_split_sum_add x5 - L106
specialize eisenstein_successor_row_split_sum_add T - L107
apply eisenstein_successor_row_split_sum_add - L108
exact hsplit_exists_witness_witness_witness_witness - L109
exact hreduced_sum_witness - L110
exact hterminal_sum_witness - L111
exact houtersum
24Establish hrestricted_columnsL112–121
Establish this local claim before using it. It is not an additional assumption.
- L112
have hrestricted_columns : ∀ eft_fixed_index_fubini_total_universal_restricted_columns. Lt(eft_fixed_index_fubini_total_universal_restricted_columns,h) → ∃ x. BetaAt(db,dc,eft_fixed_index_fubini_total_universal_restricted_columns,x) ∧ (∃ y. ∃ z. (∀ n. Lt(n,k) → ∃ m. BetaAt(y,z,n,m) ∧ (∃ i. ∃ j. ∃ u. BetaAt(bb,bc,n,i) ∧ (∀ v. Lt(v,S h) → ∃ w. BetaAt(j,u,v,w) ∧ (w = 0 ∧ (Lt(p · S n,q · S v) ∧ ¬Lt(q · S v,p · S n)) ∨ w = 1 ∧ (Lt(q · S v,p · S n) ∧ ¬Lt(p · S n,q · S v)))) ∧ BitCount(j,u,S h,i) ∧ BetaAt(j,u,eft_fixed_index_fubini_total_universal_restricted_columns,m))) ∧ BitCount(y,z,k,x))Definitions: Lt(eft_fixed_index_fubini_total_universal_restricted_columns,h)BetaAt(db,dc,eft_fixed_index_fubini_total_universal_restricted_columns,x)Lt(n,k)BetaAt(y,z,n,m)BetaAt(bb,bc,n,i)Lt(v,S h)BetaAt(j,u,v,w)Lt(p · S n,q · S v)Lt(q · S v,p · S n)BitCount(j,u,S h,i)BetaAt(j,u,eft_fixed_index_fubini_total_universal_restricted_columns,m)BitCount(y,z,k,x)Original native command in the exact edition - L113
specialize eisenstein_fubini_column_count_prefix_succ_restrict p - L114
specialize eisenstein_fubini_column_count_prefix_succ_restrict q - L115
specialize eisenstein_fubini_column_count_prefix_succ_restrict h - L116
specialize eisenstein_fubini_column_count_prefix_succ_restrict (S h) - L117
specialize eisenstein_fubini_column_count_prefix_succ_restrict bb - L118
specialize eisenstein_fubini_column_count_prefix_succ_restrict bc - L119
specialize eisenstein_fubini_column_count_prefix_succ_restrict db - L120
specialize eisenstein_fubini_column_count_prefix_succ_restrict dc - L121
specialize eisenstein_fubini_column_count_prefix_succ_restrict k
25Use earlier factsL122–122
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L122
apply eisenstein_fubini_column_count_prefix_succ_restrict
26Calculate and transport equalitiesL123–123
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L123
refl
27Use earlier factsL124–124
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L124
exact hcolumns
28Establish hreduced_columnsL125–134
Establish this local claim before using it. It is not an additional assumption.
- L125
have hreduced_columns : ∀ eft_fixed_index_fubini_total_universal_reduced_columns. Lt(eft_fixed_index_fubini_total_universal_reduced_columns,h) → ∃ y. BetaAt(db,dc,eft_fixed_index_fubini_total_universal_reduced_columns,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,k) → ∃ i. BetaAt(z,n,m,i) ∧ (∃ j. ∃ u. ∃ v. BetaAt(x,x1,m,j) ∧ (∀ w. Lt(w,h) → ∃ x0. BetaAt(u,v,w,x0) ∧ (x0 = 0 ∧ (Lt(p · S m,q · S w) ∧ ¬Lt(q · S w,p · S m)) ∨ x0 = 1 ∧ (Lt(q · S w,p · S m) ∧ ¬Lt(p · S m,q · S w)))) ∧ BitCount(u,v,h,j) ∧ BetaAt(u,v,eft_fixed_index_fubini_total_universal_reduced_columns,i))) ∧ BitCount(z,n,k,y))Definitions: Lt(eft_fixed_index_fubini_total_universal_reduced_columns,h)BetaAt(db,dc,eft_fixed_index_fubini_total_universal_reduced_columns,y)Lt(m,k)BetaAt(z,n,m,i)BetaAt(x,x1,m,j)Lt(w,h)BetaAt(u,v,w,x0)Lt(p · S m,q · S w)Lt(q · S w,p · S m)BitCount(u,v,h,j)BetaAt(u,v,eft_fixed_index_fubini_total_universal_reduced_columns,i)BitCount(z,n,k,y)Original native command in the exact edition - L126
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor p - L127
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor q - L128
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor h - L129
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor (S h) - L130
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor bb - L131
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor bc - L132
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor x - L133
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor x1 - L134
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor db
29Use earlier factsL135–137
Instantiate or apply named facts and discharge the corresponding proof obligations.
30Calculate and transport equalitiesL138–138
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L138
refl
31Use earlier factsL139–140
32Establish hsum_decomposeL141–147
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.
- L141
have hsum_decompose : ∃ a. ∃ r. BetaAt(db,dc,h,a) ∧ (Sum(db,dc,h,r) ∧ M = r + a)Definitions: BetaAt(db,dc,h,a)Sum(db,dc,h,r)Original native command in the exact edition - L142
specialize beta_sum_succ_decompose db - L143
specialize beta_sum_succ_decompose dc - L144
specialize beta_sum_succ_decompose h - L145
specialize beta_sum_succ_decompose M - L146
apply beta_sum_succ_decompose - L147
exact hcolumnsum
33Separate the logical casesL148–151
34Establish hihL152–161
35Use earlier factsL162–166
36Establish hlast_storedL167–171
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hcolumns.
- L167
have hlast_stored : ∃ n. BetaAt(db,dc,h,n) ∧ (∃ x. ∃ y. (∀ z. Lt(z,k) → ∃ m. BetaAt(x,y,z,m) ∧ (∃ i. ∃ j. ∃ u. BetaAt(bb,bc,z,i) ∧ (∀ v. Lt(v,S h) → ∃ w. BetaAt(j,u,v,w) ∧ (w = 0 ∧ (Lt(p · S z,q · S v) ∧ ¬Lt(q · S v,p · S z)) ∨ w = 1 ∧ (Lt(q · S v,p · S z) ∧ ¬Lt(p · S z,q · S v)))) ∧ BitCount(j,u,S h,i) ∧ BetaAt(j,u,h,m))) ∧ BitCount(x,y,k,n))Definitions: BetaAt(db,dc,h,n)Lt(z,k)BetaAt(x,y,z,m)BetaAt(bb,bc,z,i)Lt(v,S h)BetaAt(j,u,v,w)Lt(p · S z,q · S v)Lt(q · S v,p · S z)BitCount(j,u,S h,i)BetaAt(j,u,h,m)BitCount(x,y,k,n)Original native command in the exact edition - L168
specialize hcolumns h - L169
apply hcolumns - L170
specialize le_refl (S h) - L171
exact le_refl
37Separate the logical casesL172–177
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
38Establish hcount_eqL178–186
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
39Establish hterminal_eqL187–196
Establish this local claim before using it. It is not an additional assumption.
- L187
have hterminal_eq : x5 = x8 - L188
specialize eisenstein_successor_terminal_sum_matches_last_column p - L189
specialize eisenstein_successor_terminal_sum_matches_last_column q - L190
specialize eisenstein_successor_terminal_sum_matches_last_column h - L191
specialize eisenstein_successor_terminal_sum_matches_last_column (S h) - L192
specialize eisenstein_successor_terminal_sum_matches_last_column bb - L193
specialize eisenstein_successor_terminal_sum_matches_last_column bc - L194
specialize eisenstein_successor_terminal_sum_matches_last_column x - L195
specialize eisenstein_successor_terminal_sum_matches_last_column x1 - L196
specialize eisenstein_successor_terminal_sum_matches_last_column x2
40Use earlier factsL197–203
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L197
specialize eisenstein_successor_terminal_sum_matches_last_column x3 - L198
specialize eisenstein_successor_terminal_sum_matches_last_column x9 - L199
specialize eisenstein_successor_terminal_sum_matches_last_column x10 - L200
specialize eisenstein_successor_terminal_sum_matches_last_column k - L201
specialize eisenstein_successor_terminal_sum_matches_last_column x5 - L202
specialize eisenstein_successor_terminal_sum_matches_last_column x8 - L203
apply eisenstein_successor_terminal_sum_matches_last_column
41Calculate and transport equalitiesL204–204
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L204
refl
42Use earlier factsL205–208
43Establish htotalL209–216
Establish this local claim before using it. It is not an additional assumption.
- L209
have htotal : M = x4 + x5 - L210
rewrite hih at hsum_decompose_witness_witness_right_right - L211
rewrite <- hcount_eq at hsum_decompose_witness_witness_right_right - L212
rewrite <- hterminal_eq at hsum_decompose_witness_witness_right_right - L213
exact hsum_decompose_witness_witness_right_right - L214
trans x4 + x5 - L215
exact htotal - L216
exact hsource_add
Original defined command ledger · 216 lines
- 0001
intro h - 0002
induction h - 0003
intro p - 0004
intro q - 0005
intro k - 0006
intro bb - 0007
intro bc - 0008
intro db - 0009
intro dc - 0010
intro T - 0011
intro M - 0012
intro houter - 0013
intro hcolumns - 0014
intro houtersum - 0015
intro hcolumnsum - 0016
have hmzero : M = 0 - 0017
specialize beta_sum_zero db - 0018
specialize beta_sum_zero dc - 0019
specialize beta_sum_zero M - 0020
apply beta_sum_zero - 0021
exact hcolumnsum - 0022
have htzero : T = 0 - 0023
specialize eisenstein_zero_width_rectangle_sum_zero q - 0024
specialize eisenstein_zero_width_rectangle_sum_zero p - 0025
specialize eisenstein_zero_width_rectangle_sum_zero 0 - 0026
specialize eisenstein_zero_width_rectangle_sum_zero bb - 0027
specialize eisenstein_zero_width_rectangle_sum_zero bc - 0028
specialize eisenstein_zero_width_rectangle_sum_zero k - 0029
specialize eisenstein_zero_width_rectangle_sum_zero T - 0030
apply eisenstein_zero_width_rectangle_sum_zero - 0031
refl - 0032
exact houter - 0033
exact houtersum - 0034
trans 0 - 0035
exact hmzero - 0036
symm - 0037
exact htzero - 0038
intro p - 0039
intro q - 0040
intro k - 0041
intro bb - 0042
intro bc - 0043
intro db - 0044
intro dc - 0045
intro T - 0046
intro M - 0047
intro houter - 0048
intro hcolumns - 0049
intro houtersum - 0050
intro hcolumnsum - 0051
have hsplit_exists : ∃ rb. ∃ rc. ∃ tb. ∃ tc. ∀ x. Lt(x,k) → ∃ y. ∃ z. ∃ n. BetaAt(bb,bc,x,y) ∧ BetaAt(rb,rc,x,z) ∧ BetaAt(tb,tc,x,n) ∧ (∃ m. ∃ i. (∀ j. Lt(j,S h) → ∃ u. BetaAt(m,i,j,u) ∧ (u = 0 ∧ (Lt(p · S x,q · S j) ∧ ¬Lt(q · S j,p · S x)) ∨ u = 1 ∧ (Lt(q · S j,p · S x) ∧ ¬Lt(p · S x,q · S j)))) ∧ BitCount(m,i,S h,y) ∧ ((∀ j. Lt(j,h) → ∃ u. BetaAt(m,i,j,u) ∧ (u = 0 ∧ (Lt(p · S x,q · S j) ∧ ¬Lt(q · S j,p · S x)) ∨ u = 1 ∧ (Lt(q · S j,p · S x) ∧ ¬Lt(p · S x,q · S j)))) ∧ BetaAt(m,i,h,n)) ∧ (BitCount(m,i,h,z) ∧ (n = 0 ∨ n = 1) ∧ y = z + n))Exact native replay line
have hsplit_exists : exists rb rc tb tc. (forall efrd_row_index_fubini_total_universal_split_exists. (exists efrd_lt_gap_fubini_total_universal_split_exists_bound. efrd_lt_gap_fubini_total_universal_split_exists_bound + S (efrd_row_index_fubini_total_universal_split_exists) = k) -> exists efrd_count_fubini_total_universal_split_exists efrd_reduced_count_fubini_total_universal_split_exists efrd_terminal_bit_fubini_total_universal_split_exists. (((((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_outer_entry. ff_h_efrd_fubini_total_universal_split_exists_entry_outer_entry + S (efrd_count_fubini_total_universal_split_exists) = S ((S (efrd_row_index_fubini_total_universal_split_exists)) * bc)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_outer_entry. bb = ff_q_efrd_fubini_total_universal_split_exists_entry_outer_entry * S ((S (efrd_row_index_fubini_total_universal_split_exists)) * bc) + (efrd_count_fubini_total_universal_split_exists))) /\ (((exists ff_h_efrd_fubini_total_universal_split_exists_entry_reduced_entry. ff_h_efrd_fubini_total_universal_split_exists_entry_reduced_entry + S (efrd_reduced_count_fubini_total_universal_split_exists) = S ((S (efrd_row_index_fubini_total_universal_split_exists)) * rc)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_reduced_entry. rb = ff_q_efrd_fubini_total_universal_split_exists_entry_reduced_entry * S ((S (efrd_row_index_fubini_total_universal_split_exists)) * rc) + (efrd_reduced_count_fubini_total_universal_split_exists)))) /\ (((exists ff_h_efrd_fubini_total_universal_split_exists_entry_terminal_entry. ff_h_efrd_fubini_total_universal_split_exists_entry_terminal_entry + S (efrd_terminal_bit_fubini_total_universal_split_exists) = S ((S (efrd_row_index_fubini_total_universal_split_exists)) * tc)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_terminal_entry. tb = ff_q_efrd_fubini_total_universal_split_exists_entry_terminal_entry * S ((S (efrd_row_index_fubini_total_universal_split_exists)) * tc) + (efrd_terminal_bit_fubini_total_universal_split_exists)))) /\ (exists efrd_row_code_fubini_total_universal_split_exists_entry_split efrd_row_scale_fubini_total_universal_split_exists_entry_split. (((((forall eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix. (exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_bound. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_bound + S (eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix) = S h) -> exists eri_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix) = S ((S (eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_eri_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_decoded. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_eri_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (eri_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_left + S (p * S efrd_row_index_fubini_total_universal_split_exists) = q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_right + S (q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix) = p * S efrd_row_index_fubini_total_universal_split_exists))) \/ (eri_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_right + S (q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix) = p * S efrd_row_index_fubini_total_universal_split_exists) /\ ~(exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_left + S (p * S efrd_row_index_fubini_total_universal_split_exists) = q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_start. ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_start. ff_u_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_terminal. ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_terminal + S (efrd_count_fubini_total_universal_split_exists) = S ((S (S h)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_terminal. ff_u_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_terminal * S ((S (S h)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) + (efrd_count_fubini_total_universal_split_exists))) /\ forall ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum. (exists ff_lt_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_bound. ff_lt_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_bound + S ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum = S h) -> exists ff_a_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum ff_r_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum ff_s_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_summand. ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_summand + S (ff_a_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_summand. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (ff_a_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_partial. ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_partial + S (ff_r_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_partial. ff_u_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) + (ff_r_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_successor. ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_successor + S (ff_s_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_successor. ff_u_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) + (ff_s_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum))) /\ ff_s_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum = ff_r_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum + ff_a_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits. (exists ff_lt_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits_bound. ff_lt_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits_bound + S ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits = S h) -> exists ff_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits. ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits_decoded. ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits_decoded. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (ff_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix. (exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_bound. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_bound + S (eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_eri_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_decoded. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_eri_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (eri_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_left + S (p * S efrd_row_index_fubini_total_universal_split_exists) = q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_right + S (q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix) = p * S efrd_row_index_fubini_total_universal_split_exists))) \/ (eri_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_right + S (q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix) = p * S efrd_row_index_fubini_total_universal_split_exists) /\ ~(exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_left + S (p * S efrd_row_index_fubini_total_universal_split_exists) = q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_terminal_entry. ff_h_efrd_fubini_total_universal_split_exists_entry_split_terminal_entry + S (efrd_terminal_bit_fubini_total_universal_split_exists) = S ((S (h)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_terminal_entry. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_efrd_fubini_total_universal_split_exists_entry_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (efrd_terminal_bit_fubini_total_universal_split_exists))))) /\ (((((exists ff_u_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_start. ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_start. ff_u_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_terminal. ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_total_universal_split_exists) = S ((S (h)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_terminal. ff_u_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) + (efrd_reduced_count_fubini_total_universal_split_exists))) /\ forall ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum. (exists ff_lt_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_bound. ff_lt_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_bound + S ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum ff_r_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum ff_s_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_summand. ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_summand. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (ff_a_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_partial. ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_partial. ff_u_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) + (ff_r_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_successor. ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_successor. ff_u_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) + (ff_s_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum))) /\ ff_s_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum = ff_r_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum + ff_a_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits. (exists ff_lt_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits_bound. ff_lt_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits_bound + S ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits_decoded. ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits_decoded. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (ff_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_total_universal_split_exists = 0 \/ efrd_terminal_bit_fubini_total_universal_split_exists = 1)) /\ efrd_count_fubini_total_universal_split_exists = efrd_reduced_count_fubini_total_universal_split_exists + efrd_terminal_bit_fubini_total_universal_split_exists))))))) - 0052
specialize eisenstein_successor_rectangle_row_split_prefix_exists q - 0053
specialize eisenstein_successor_rectangle_row_split_prefix_exists p - 0054
specialize eisenstein_successor_rectangle_row_split_prefix_exists h - 0055
specialize eisenstein_successor_rectangle_row_split_prefix_exists (S h) - 0056
specialize eisenstein_successor_rectangle_row_split_prefix_exists bb - 0057
specialize eisenstein_successor_rectangle_row_split_prefix_exists bc - 0058
specialize eisenstein_successor_rectangle_row_split_prefix_exists k - 0059
apply eisenstein_successor_rectangle_row_split_prefix_exists - 0060
refl - 0061
exact houter - 0062
cases hsplit_exists - 0063
cases hsplit_exists_witness - 0064
cases hsplit_exists_witness_witness - 0065
cases hsplit_exists_witness_witness_witness - 0066
have hreduced_outer : ∀ erc_row_fubini_total_universal_reduced_outer. Lt(erc_row_fubini_total_universal_reduced_outer,k) → ∃ y. BetaAt(x,x1,erc_row_fubini_total_universal_reduced_outer,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,h) → ∃ i. BetaAt(z,n,m,i) ∧ (i = 0 ∧ (Lt(p · S erc_row_fubini_total_universal_reduced_outer,q · S m) ∧ ¬Lt(q · S m,p · S erc_row_fubini_total_universal_reduced_outer)) ∨ i = 1 ∧ (Lt(q · S m,p · S erc_row_fubini_total_universal_reduced_outer) ∧ ¬Lt(p · S erc_row_fubini_total_universal_reduced_outer,q · S m)))) ∧ BitCount(z,n,h,y))Exact native replay line
have hreduced_outer : forall erc_row_fubini_total_universal_reduced_outer. (exists erc_lt_gap_fubini_total_universal_reduced_outer_bound. erc_lt_gap_fubini_total_universal_reduced_outer_bound + S (erc_row_fubini_total_universal_reduced_outer) = k) -> exists erc_count_fubini_total_universal_reduced_outer. ((((exists ff_h_erc_fubini_total_universal_reduced_outer_decoded. ff_h_erc_fubini_total_universal_reduced_outer_decoded + S (erc_count_fubini_total_universal_reduced_outer) = S ((S (erc_row_fubini_total_universal_reduced_outer)) * x1)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_decoded. x = ff_q_erc_fubini_total_universal_reduced_outer_decoded * S ((S (erc_row_fubini_total_universal_reduced_outer)) * x1) + (erc_count_fubini_total_universal_reduced_outer))) /\ (exists erc_row_code_fubini_total_universal_reduced_outer_witness erc_row_scale_fubini_total_universal_reduced_outer_witness. ((forall eri_column_erc_fubini_total_universal_reduced_outer_witness_row. (exists eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_bound. eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_bound + S (eri_column_erc_fubini_total_universal_reduced_outer_witness_row) = h) -> exists eri_bit_erc_fubini_total_universal_reduced_outer_witness_row. ((((exists ff_h_eri_erc_fubini_total_universal_reduced_outer_witness_row_decoded. ff_h_eri_erc_fubini_total_universal_reduced_outer_witness_row_decoded + S (eri_bit_erc_fubini_total_universal_reduced_outer_witness_row) = S ((S (eri_column_erc_fubini_total_universal_reduced_outer_witness_row)) * erc_row_scale_fubini_total_universal_reduced_outer_witness)) /\ exists ff_q_eri_erc_fubini_total_universal_reduced_outer_witness_row_decoded. erc_row_code_fubini_total_universal_reduced_outer_witness = ff_q_eri_erc_fubini_total_universal_reduced_outer_witness_row_decoded * S ((S (eri_column_erc_fubini_total_universal_reduced_outer_witness_row)) * erc_row_scale_fubini_total_universal_reduced_outer_witness) + (eri_bit_erc_fubini_total_universal_reduced_outer_witness_row))) /\ (((eri_bit_erc_fubini_total_universal_reduced_outer_witness_row = 0 /\ ((exists eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_left. eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_universal_reduced_outer) = q * S eri_column_erc_fubini_total_universal_reduced_outer_witness_row) /\ ~(exists eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_right. eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_universal_reduced_outer_witness_row) = p * S erc_row_fubini_total_universal_reduced_outer))) \/ (eri_bit_erc_fubini_total_universal_reduced_outer_witness_row = 1 /\ ((exists eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_right. eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_universal_reduced_outer_witness_row) = p * S erc_row_fubini_total_universal_reduced_outer) /\ ~(exists eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_left. eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_universal_reduced_outer) = q * S eri_column_erc_fubini_total_universal_reduced_outer_witness_row))))))) /\ (((exists ff_u_erc_fubini_total_universal_reduced_outer_witness_count_sum ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_start. ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_start. ff_u_erc_fubini_total_universal_reduced_outer_witness_count_sum = ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_terminal. ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_terminal + S (erc_count_fubini_total_universal_reduced_outer) = S ((S (h)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_terminal. ff_u_erc_fubini_total_universal_reduced_outer_witness_count_sum = ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_terminal * S ((S (h)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum) + (erc_count_fubini_total_universal_reduced_outer))) /\ forall ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum. (exists ff_lt_erc_fubini_total_universal_reduced_outer_witness_count_sum_bound. ff_lt_erc_fubini_total_universal_reduced_outer_witness_count_sum_bound + S ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum = h) -> exists ff_a_erc_fubini_total_universal_reduced_outer_witness_count_sum ff_r_erc_fubini_total_universal_reduced_outer_witness_count_sum ff_s_erc_fubini_total_universal_reduced_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_summand. ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_summand + S (ff_a_erc_fubini_total_universal_reduced_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum)) * erc_row_scale_fubini_total_universal_reduced_outer_witness)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_summand. erc_row_code_fubini_total_universal_reduced_outer_witness = ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_summand * S ((S (ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum)) * erc_row_scale_fubini_total_universal_reduced_outer_witness) + (ff_a_erc_fubini_total_universal_reduced_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_partial. ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_partial + S (ff_r_erc_fubini_total_universal_reduced_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_partial. ff_u_erc_fubini_total_universal_reduced_outer_witness_count_sum = ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_partial * S ((S (ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum) + (ff_r_erc_fubini_total_universal_reduced_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_successor. ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_successor + S (ff_s_erc_fubini_total_universal_reduced_outer_witness_count_sum) = S ((S (S ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_successor. ff_u_erc_fubini_total_universal_reduced_outer_witness_count_sum = ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum) + (ff_s_erc_fubini_total_universal_reduced_outer_witness_count_sum))) /\ ff_s_erc_fubini_total_universal_reduced_outer_witness_count_sum = ff_r_erc_fubini_total_universal_reduced_outer_witness_count_sum + ff_a_erc_fubini_total_universal_reduced_outer_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_total_universal_reduced_outer_witness_count_bits. (exists ff_lt_erc_fubini_total_universal_reduced_outer_witness_count_bits_bound. ff_lt_erc_fubini_total_universal_reduced_outer_witness_count_bits_bound + S ff_i_erc_fubini_total_universal_reduced_outer_witness_count_bits = h) -> exists ff_bit_erc_fubini_total_universal_reduced_outer_witness_count_bits. ((((exists ff_h_erc_fubini_total_universal_reduced_outer_witness_count_bits_decoded. ff_h_erc_fubini_total_universal_reduced_outer_witness_count_bits_decoded + S (ff_bit_erc_fubini_total_universal_reduced_outer_witness_count_bits) = S ((S (ff_i_erc_fubini_total_universal_reduced_outer_witness_count_bits)) * erc_row_scale_fubini_total_universal_reduced_outer_witness)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_witness_count_bits_decoded. erc_row_code_fubini_total_universal_reduced_outer_witness = ff_q_erc_fubini_total_universal_reduced_outer_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_total_universal_reduced_outer_witness_count_bits)) * erc_row_scale_fubini_total_universal_reduced_outer_witness) + (ff_bit_erc_fubini_total_universal_reduced_outer_witness_count_bits))) /\ (ff_bit_erc_fubini_total_universal_reduced_outer_witness_count_bits = 0 \/ ff_bit_erc_fubini_total_universal_reduced_outer_witness_count_bits = 1)))))))) - 0067
specialize eisenstein_successor_row_split_reduced_rectangle_prefix q - 0068
specialize eisenstein_successor_row_split_reduced_rectangle_prefix p - 0069
specialize eisenstein_successor_row_split_reduced_rectangle_prefix h - 0070
specialize eisenstein_successor_row_split_reduced_rectangle_prefix (S h) - 0071
specialize eisenstein_successor_row_split_reduced_rectangle_prefix bb - 0072
specialize eisenstein_successor_row_split_reduced_rectangle_prefix bc - 0073
specialize eisenstein_successor_row_split_reduced_rectangle_prefix x - 0074
specialize eisenstein_successor_row_split_reduced_rectangle_prefix x1 - 0075
specialize eisenstein_successor_row_split_reduced_rectangle_prefix x2 - 0076
specialize eisenstein_successor_row_split_reduced_rectangle_prefix x3 - 0077
specialize eisenstein_successor_row_split_reduced_rectangle_prefix k - 0078
apply eisenstein_successor_row_split_reduced_rectangle_prefix - 0079
exact hsplit_exists_witness_witness_witness_witness - 0080
have hreduced_sum : ∃ R. Sum(x,x1,k,R)Exact native replay line
have hreduced_sum : exists R. (exists ff_u_fubini_total_universal_reduced_sum ff_v_fubini_total_universal_reduced_sum. ((((exists ff_h_fubini_total_universal_reduced_sum_start. ff_h_fubini_total_universal_reduced_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_universal_reduced_sum)) /\ exists ff_q_fubini_total_universal_reduced_sum_start. ff_u_fubini_total_universal_reduced_sum = ff_q_fubini_total_universal_reduced_sum_start * S ((S (0)) * ff_v_fubini_total_universal_reduced_sum) + (0))) /\ ((((exists ff_h_fubini_total_universal_reduced_sum_terminal. ff_h_fubini_total_universal_reduced_sum_terminal + S (R) = S ((S (k)) * ff_v_fubini_total_universal_reduced_sum)) /\ exists ff_q_fubini_total_universal_reduced_sum_terminal. ff_u_fubini_total_universal_reduced_sum = ff_q_fubini_total_universal_reduced_sum_terminal * S ((S (k)) * ff_v_fubini_total_universal_reduced_sum) + (R))) /\ forall ff_i_fubini_total_universal_reduced_sum. (exists ff_lt_fubini_total_universal_reduced_sum_bound. ff_lt_fubini_total_universal_reduced_sum_bound + S ff_i_fubini_total_universal_reduced_sum = k) -> exists ff_a_fubini_total_universal_reduced_sum ff_r_fubini_total_universal_reduced_sum ff_s_fubini_total_universal_reduced_sum. ((((exists ff_h_fubini_total_universal_reduced_sum_summand. ff_h_fubini_total_universal_reduced_sum_summand + S (ff_a_fubini_total_universal_reduced_sum) = S ((S (ff_i_fubini_total_universal_reduced_sum)) * x1)) /\ exists ff_q_fubini_total_universal_reduced_sum_summand. x = ff_q_fubini_total_universal_reduced_sum_summand * S ((S (ff_i_fubini_total_universal_reduced_sum)) * x1) + (ff_a_fubini_total_universal_reduced_sum))) /\ ((((exists ff_h_fubini_total_universal_reduced_sum_partial. ff_h_fubini_total_universal_reduced_sum_partial + S (ff_r_fubini_total_universal_reduced_sum) = S ((S (ff_i_fubini_total_universal_reduced_sum)) * ff_v_fubini_total_universal_reduced_sum)) /\ exists ff_q_fubini_total_universal_reduced_sum_partial. ff_u_fubini_total_universal_reduced_sum = ff_q_fubini_total_universal_reduced_sum_partial * S ((S (ff_i_fubini_total_universal_reduced_sum)) * ff_v_fubini_total_universal_reduced_sum) + (ff_r_fubini_total_universal_reduced_sum))) /\ ((((exists ff_h_fubini_total_universal_reduced_sum_successor. ff_h_fubini_total_universal_reduced_sum_successor + S (ff_s_fubini_total_universal_reduced_sum) = S ((S (S ff_i_fubini_total_universal_reduced_sum)) * ff_v_fubini_total_universal_reduced_sum)) /\ exists ff_q_fubini_total_universal_reduced_sum_successor. ff_u_fubini_total_universal_reduced_sum = ff_q_fubini_total_universal_reduced_sum_successor * S ((S (S ff_i_fubini_total_universal_reduced_sum)) * ff_v_fubini_total_universal_reduced_sum) + (ff_s_fubini_total_universal_reduced_sum))) /\ ff_s_fubini_total_universal_reduced_sum = ff_r_fubini_total_universal_reduced_sum + ff_a_fubini_total_universal_reduced_sum)))))) - 0081
specialize beta_sum_exists x - 0082
specialize beta_sum_exists x1 - 0083
specialize beta_sum_exists k - 0084
exact beta_sum_exists - 0085
cases hreduced_sum - 0086
have hterminal_sum : ∃ D. Sum(x2,x3,k,D)Exact native replay line
have hterminal_sum : exists D. (exists ff_u_fubini_total_universal_terminal_sum ff_v_fubini_total_universal_terminal_sum. ((((exists ff_h_fubini_total_universal_terminal_sum_start. ff_h_fubini_total_universal_terminal_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_universal_terminal_sum)) /\ exists ff_q_fubini_total_universal_terminal_sum_start. ff_u_fubini_total_universal_terminal_sum = ff_q_fubini_total_universal_terminal_sum_start * S ((S (0)) * ff_v_fubini_total_universal_terminal_sum) + (0))) /\ ((((exists ff_h_fubini_total_universal_terminal_sum_terminal. ff_h_fubini_total_universal_terminal_sum_terminal + S (D) = S ((S (k)) * ff_v_fubini_total_universal_terminal_sum)) /\ exists ff_q_fubini_total_universal_terminal_sum_terminal. ff_u_fubini_total_universal_terminal_sum = ff_q_fubini_total_universal_terminal_sum_terminal * S ((S (k)) * ff_v_fubini_total_universal_terminal_sum) + (D))) /\ forall ff_i_fubini_total_universal_terminal_sum. (exists ff_lt_fubini_total_universal_terminal_sum_bound. ff_lt_fubini_total_universal_terminal_sum_bound + S ff_i_fubini_total_universal_terminal_sum = k) -> exists ff_a_fubini_total_universal_terminal_sum ff_r_fubini_total_universal_terminal_sum ff_s_fubini_total_universal_terminal_sum. ((((exists ff_h_fubini_total_universal_terminal_sum_summand. ff_h_fubini_total_universal_terminal_sum_summand + S (ff_a_fubini_total_universal_terminal_sum) = S ((S (ff_i_fubini_total_universal_terminal_sum)) * x3)) /\ exists ff_q_fubini_total_universal_terminal_sum_summand. x2 = ff_q_fubini_total_universal_terminal_sum_summand * S ((S (ff_i_fubini_total_universal_terminal_sum)) * x3) + (ff_a_fubini_total_universal_terminal_sum))) /\ ((((exists ff_h_fubini_total_universal_terminal_sum_partial. ff_h_fubini_total_universal_terminal_sum_partial + S (ff_r_fubini_total_universal_terminal_sum) = S ((S (ff_i_fubini_total_universal_terminal_sum)) * ff_v_fubini_total_universal_terminal_sum)) /\ exists ff_q_fubini_total_universal_terminal_sum_partial. ff_u_fubini_total_universal_terminal_sum = ff_q_fubini_total_universal_terminal_sum_partial * S ((S (ff_i_fubini_total_universal_terminal_sum)) * ff_v_fubini_total_universal_terminal_sum) + (ff_r_fubini_total_universal_terminal_sum))) /\ ((((exists ff_h_fubini_total_universal_terminal_sum_successor. ff_h_fubini_total_universal_terminal_sum_successor + S (ff_s_fubini_total_universal_terminal_sum) = S ((S (S ff_i_fubini_total_universal_terminal_sum)) * ff_v_fubini_total_universal_terminal_sum)) /\ exists ff_q_fubini_total_universal_terminal_sum_successor. ff_u_fubini_total_universal_terminal_sum = ff_q_fubini_total_universal_terminal_sum_successor * S ((S (S ff_i_fubini_total_universal_terminal_sum)) * ff_v_fubini_total_universal_terminal_sum) + (ff_s_fubini_total_universal_terminal_sum))) /\ ff_s_fubini_total_universal_terminal_sum = ff_r_fubini_total_universal_terminal_sum + ff_a_fubini_total_universal_terminal_sum)))))) - 0087
specialize beta_sum_exists x2 - 0088
specialize beta_sum_exists x3 - 0089
specialize beta_sum_exists k - 0090
exact beta_sum_exists - 0091
cases hterminal_sum - 0092
have hsource_add : x4 + x5 = T - 0093
specialize eisenstein_successor_row_split_sum_add q - 0094
specialize eisenstein_successor_row_split_sum_add p - 0095
specialize eisenstein_successor_row_split_sum_add h - 0096
specialize eisenstein_successor_row_split_sum_add (S h) - 0097
specialize eisenstein_successor_row_split_sum_add bb - 0098
specialize eisenstein_successor_row_split_sum_add bc - 0099
specialize eisenstein_successor_row_split_sum_add x - 0100
specialize eisenstein_successor_row_split_sum_add x1 - 0101
specialize eisenstein_successor_row_split_sum_add x2 - 0102
specialize eisenstein_successor_row_split_sum_add x3 - 0103
specialize eisenstein_successor_row_split_sum_add k - 0104
specialize eisenstein_successor_row_split_sum_add x4 - 0105
specialize eisenstein_successor_row_split_sum_add x5 - 0106
specialize eisenstein_successor_row_split_sum_add T - 0107
apply eisenstein_successor_row_split_sum_add - 0108
exact hsplit_exists_witness_witness_witness_witness - 0109
exact hreduced_sum_witness - 0110
exact hterminal_sum_witness - 0111
exact houtersum - 0112
have hrestricted_columns : ∀ eft_fixed_index_fubini_total_universal_restricted_columns. Lt(eft_fixed_index_fubini_total_universal_restricted_columns,h) → ∃ x. BetaAt(db,dc,eft_fixed_index_fubini_total_universal_restricted_columns,x) ∧ (∃ y. ∃ z. (∀ n. Lt(n,k) → ∃ m. BetaAt(y,z,n,m) ∧ (∃ i. ∃ j. ∃ u. BetaAt(bb,bc,n,i) ∧ (∀ v. Lt(v,S h) → ∃ w. BetaAt(j,u,v,w) ∧ (w = 0 ∧ (Lt(p · S n,q · S v) ∧ ¬Lt(q · S v,p · S n)) ∨ w = 1 ∧ (Lt(q · S v,p · S n) ∧ ¬Lt(p · S n,q · S v)))) ∧ BitCount(j,u,S h,i) ∧ BetaAt(j,u,eft_fixed_index_fubini_total_universal_restricted_columns,m))) ∧ BitCount(y,z,k,x))Exact native replay line
have hrestricted_columns : forall eft_fixed_index_fubini_total_universal_restricted_columns. (exists edt_lt_gap_eft_fubini_total_universal_restricted_columns_bound. edt_lt_gap_eft_fubini_total_universal_restricted_columns_bound + S (eft_fixed_index_fubini_total_universal_restricted_columns) = h) -> exists eft_count_fubini_total_universal_restricted_columns. ((((exists ff_h_eft_fubini_total_universal_restricted_columns_decoded. ff_h_eft_fubini_total_universal_restricted_columns_decoded + S (eft_count_fubini_total_universal_restricted_columns) = S ((S (eft_fixed_index_fubini_total_universal_restricted_columns)) * dc)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_decoded. db = ff_q_eft_fubini_total_universal_restricted_columns_decoded * S ((S (eft_fixed_index_fubini_total_universal_restricted_columns)) * dc) + (eft_count_fubini_total_universal_restricted_columns))) /\ (exists eft_column_code_fubini_total_universal_restricted_columns_witness eft_column_scale_fubini_total_universal_restricted_columns_witness. ((forall etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column. (exists edt_lt_gap_eft_fubini_total_universal_restricted_columns_witness_column_bound. edt_lt_gap_eft_fubini_total_universal_restricted_columns_witness_column_bound + S (etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column) = k) -> exists etc_bit_eft_fubini_total_universal_restricted_columns_witness_column. ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_decoded. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_decoded + S (etc_bit_eft_fubini_total_universal_restricted_columns_witness_column) = S ((S (etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column)) * eft_column_scale_fubini_total_universal_restricted_columns_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_decoded. eft_column_code_fubini_total_universal_restricted_columns_witness = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_decoded * S ((S (etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column)) * eft_column_scale_fubini_total_universal_restricted_columns_witness) + (etc_bit_eft_fubini_total_universal_restricted_columns_witness_column))) /\ (exists etc_count_eft_fubini_total_universal_restricted_columns_witness_column_witness etc_row_code_eft_fubini_total_universal_restricted_columns_witness_column_witness etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness. ((((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_outer_entry. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_outer_entry + S (etc_count_eft_fubini_total_universal_restricted_columns_witness_column_witness) = S ((S (etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column)) * bc)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_outer_entry. bb = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_outer_entry * S ((S (etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column)) * bc) + (etc_count_eft_fubini_total_universal_restricted_columns_witness_column_witness))) /\ (forall eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row. (exists eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_bound. eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_bound + S (eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row) = S h) -> exists eri_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row. ((((exists ff_h_eri_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_decoded. ff_h_eri_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_decoded + S (eri_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row) = S ((S (eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness)) /\ exists ff_q_eri_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_decoded. etc_row_code_eft_fubini_total_universal_restricted_columns_witness_column_witness = ff_q_eri_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_decoded * S ((S (eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness) + (eri_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row))) /\ (((eri_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column) = q * S eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row) /\ ~(exists eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column))) \/ (eri_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column) /\ ~(exists eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column) = q * S eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_start. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_start. ff_u_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_terminal. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_terminal + S (etc_count_eft_fubini_total_universal_restricted_columns_witness_column_witness) = S ((S (S h)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_terminal. ff_u_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_terminal * S ((S (S h)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) + (etc_count_eft_fubini_total_universal_restricted_columns_witness_column_witness))) /\ forall ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum. (exists ff_lt_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_bound. ff_lt_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_bound + S ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum = S h) -> exists ff_a_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum ff_r_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum ff_s_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_summand. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_summand. etc_row_code_eft_fubini_total_universal_restricted_columns_witness_column_witness = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness) + (ff_a_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_partial. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_partial. ff_u_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) + (ff_r_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_successor. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_successor. ff_u_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) + (ff_s_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum))) /\ ff_s_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum = ff_r_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum + ff_a_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits. (exists ff_lt_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits_bound. ff_lt_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits_bound + S ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits = S h) -> exists ff_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits_decoded. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits_decoded. etc_row_code_eft_fubini_total_universal_restricted_columns_witness_column_witness = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness) + (ff_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_inner_entry. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_inner_entry + S (etc_bit_eft_fubini_total_universal_restricted_columns_witness_column) = S ((S (eft_fixed_index_fubini_total_universal_restricted_columns)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_inner_entry. etc_row_code_eft_fubini_total_universal_restricted_columns_witness_column_witness = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_inner_entry * S ((S (eft_fixed_index_fubini_total_universal_restricted_columns)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness) + (etc_bit_eft_fubini_total_universal_restricted_columns_witness_column))))))) /\ (((exists ff_u_eft_fubini_total_universal_restricted_columns_witness_count_sum ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum. ((((exists ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_start. ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_start. ff_u_eft_fubini_total_universal_restricted_columns_witness_count_sum = ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_start * S ((S (0)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum) + (0))) /\ ((((exists ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_terminal. ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_terminal + S (eft_count_fubini_total_universal_restricted_columns) = S ((S (k)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_terminal. ff_u_eft_fubini_total_universal_restricted_columns_witness_count_sum = ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_terminal * S ((S (k)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum) + (eft_count_fubini_total_universal_restricted_columns))) /\ forall ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum. (exists ff_lt_eft_fubini_total_universal_restricted_columns_witness_count_sum_bound. ff_lt_eft_fubini_total_universal_restricted_columns_witness_count_sum_bound + S ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum = k) -> exists ff_a_eft_fubini_total_universal_restricted_columns_witness_count_sum ff_r_eft_fubini_total_universal_restricted_columns_witness_count_sum ff_s_eft_fubini_total_universal_restricted_columns_witness_count_sum. ((((exists ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_summand. ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_summand + S (ff_a_eft_fubini_total_universal_restricted_columns_witness_count_sum) = S ((S (ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum)) * eft_column_scale_fubini_total_universal_restricted_columns_witness)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_summand. eft_column_code_fubini_total_universal_restricted_columns_witness = ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_summand * S ((S (ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum)) * eft_column_scale_fubini_total_universal_restricted_columns_witness) + (ff_a_eft_fubini_total_universal_restricted_columns_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_partial. ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_partial + S (ff_r_eft_fubini_total_universal_restricted_columns_witness_count_sum) = S ((S (ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_partial. ff_u_eft_fubini_total_universal_restricted_columns_witness_count_sum = ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_partial * S ((S (ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum) + (ff_r_eft_fubini_total_universal_restricted_columns_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_successor. ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_successor + S (ff_s_eft_fubini_total_universal_restricted_columns_witness_count_sum) = S ((S (S ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_successor. ff_u_eft_fubini_total_universal_restricted_columns_witness_count_sum = ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_successor * S ((S (S ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum) + (ff_s_eft_fubini_total_universal_restricted_columns_witness_count_sum))) /\ ff_s_eft_fubini_total_universal_restricted_columns_witness_count_sum = ff_r_eft_fubini_total_universal_restricted_columns_witness_count_sum + ff_a_eft_fubini_total_universal_restricted_columns_witness_count_sum)))))) /\ (forall ff_i_eft_fubini_total_universal_restricted_columns_witness_count_bits. (exists ff_lt_eft_fubini_total_universal_restricted_columns_witness_count_bits_bound. ff_lt_eft_fubini_total_universal_restricted_columns_witness_count_bits_bound + S ff_i_eft_fubini_total_universal_restricted_columns_witness_count_bits = k) -> exists ff_bit_eft_fubini_total_universal_restricted_columns_witness_count_bits. ((((exists ff_h_eft_fubini_total_universal_restricted_columns_witness_count_bits_decoded. ff_h_eft_fubini_total_universal_restricted_columns_witness_count_bits_decoded + S (ff_bit_eft_fubini_total_universal_restricted_columns_witness_count_bits) = S ((S (ff_i_eft_fubini_total_universal_restricted_columns_witness_count_bits)) * eft_column_scale_fubini_total_universal_restricted_columns_witness)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_witness_count_bits_decoded. eft_column_code_fubini_total_universal_restricted_columns_witness = ff_q_eft_fubini_total_universal_restricted_columns_witness_count_bits_decoded * S ((S (ff_i_eft_fubini_total_universal_restricted_columns_witness_count_bits)) * eft_column_scale_fubini_total_universal_restricted_columns_witness) + (ff_bit_eft_fubini_total_universal_restricted_columns_witness_count_bits))) /\ (ff_bit_eft_fubini_total_universal_restricted_columns_witness_count_bits = 0 \/ ff_bit_eft_fubini_total_universal_restricted_columns_witness_count_bits = 1)))))))) - 0113
specialize eisenstein_fubini_column_count_prefix_succ_restrict p - 0114
specialize eisenstein_fubini_column_count_prefix_succ_restrict q - 0115
specialize eisenstein_fubini_column_count_prefix_succ_restrict h - 0116
specialize eisenstein_fubini_column_count_prefix_succ_restrict (S h) - 0117
specialize eisenstein_fubini_column_count_prefix_succ_restrict bb - 0118
specialize eisenstein_fubini_column_count_prefix_succ_restrict bc - 0119
specialize eisenstein_fubini_column_count_prefix_succ_restrict db - 0120
specialize eisenstein_fubini_column_count_prefix_succ_restrict dc - 0121
specialize eisenstein_fubini_column_count_prefix_succ_restrict k - 0122
apply eisenstein_fubini_column_count_prefix_succ_restrict - 0123
refl - 0124
exact hcolumns - 0125
have hreduced_columns : ∀ eft_fixed_index_fubini_total_universal_reduced_columns. Lt(eft_fixed_index_fubini_total_universal_reduced_columns,h) → ∃ y. BetaAt(db,dc,eft_fixed_index_fubini_total_universal_reduced_columns,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,k) → ∃ i. BetaAt(z,n,m,i) ∧ (∃ j. ∃ u. ∃ v. BetaAt(x,x1,m,j) ∧ (∀ w. Lt(w,h) → ∃ x0. BetaAt(u,v,w,x0) ∧ (x0 = 0 ∧ (Lt(p · S m,q · S w) ∧ ¬Lt(q · S w,p · S m)) ∨ x0 = 1 ∧ (Lt(q · S w,p · S m) ∧ ¬Lt(p · S m,q · S w)))) ∧ BitCount(u,v,h,j) ∧ BetaAt(u,v,eft_fixed_index_fubini_total_universal_reduced_columns,i))) ∧ BitCount(z,n,k,y))Exact native replay line
have hreduced_columns : forall eft_fixed_index_fubini_total_universal_reduced_columns. (exists edt_lt_gap_eft_fubini_total_universal_reduced_columns_bound. edt_lt_gap_eft_fubini_total_universal_reduced_columns_bound + S (eft_fixed_index_fubini_total_universal_reduced_columns) = h) -> exists eft_count_fubini_total_universal_reduced_columns. ((((exists ff_h_eft_fubini_total_universal_reduced_columns_decoded. ff_h_eft_fubini_total_universal_reduced_columns_decoded + S (eft_count_fubini_total_universal_reduced_columns) = S ((S (eft_fixed_index_fubini_total_universal_reduced_columns)) * dc)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_decoded. db = ff_q_eft_fubini_total_universal_reduced_columns_decoded * S ((S (eft_fixed_index_fubini_total_universal_reduced_columns)) * dc) + (eft_count_fubini_total_universal_reduced_columns))) /\ (exists eft_column_code_fubini_total_universal_reduced_columns_witness eft_column_scale_fubini_total_universal_reduced_columns_witness. ((forall etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column. (exists edt_lt_gap_eft_fubini_total_universal_reduced_columns_witness_column_bound. edt_lt_gap_eft_fubini_total_universal_reduced_columns_witness_column_bound + S (etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column) = k) -> exists etc_bit_eft_fubini_total_universal_reduced_columns_witness_column. ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_decoded. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_decoded + S (etc_bit_eft_fubini_total_universal_reduced_columns_witness_column) = S ((S (etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column)) * eft_column_scale_fubini_total_universal_reduced_columns_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_decoded. eft_column_code_fubini_total_universal_reduced_columns_witness = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_decoded * S ((S (etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column)) * eft_column_scale_fubini_total_universal_reduced_columns_witness) + (etc_bit_eft_fubini_total_universal_reduced_columns_witness_column))) /\ (exists etc_count_eft_fubini_total_universal_reduced_columns_witness_column_witness etc_row_code_eft_fubini_total_universal_reduced_columns_witness_column_witness etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness. ((((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_outer_entry. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_outer_entry + S (etc_count_eft_fubini_total_universal_reduced_columns_witness_column_witness) = S ((S (etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column)) * x1)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_outer_entry. x = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_outer_entry * S ((S (etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column)) * x1) + (etc_count_eft_fubini_total_universal_reduced_columns_witness_column_witness))) /\ (forall eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row. (exists eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_bound. eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_bound + S (eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row) = h) -> exists eri_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row. ((((exists ff_h_eri_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_decoded. ff_h_eri_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_decoded + S (eri_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row) = S ((S (eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness)) /\ exists ff_q_eri_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_decoded. etc_row_code_eft_fubini_total_universal_reduced_columns_witness_column_witness = ff_q_eri_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_decoded * S ((S (eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness) + (eri_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row))) /\ (((eri_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column) = q * S eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row) /\ ~(exists eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column))) \/ (eri_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column) /\ ~(exists eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column) = q * S eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_start. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_start. ff_u_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_terminal. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_terminal + S (etc_count_eft_fubini_total_universal_reduced_columns_witness_column_witness) = S ((S (h)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_terminal. ff_u_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) + (etc_count_eft_fubini_total_universal_reduced_columns_witness_column_witness))) /\ forall ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum. (exists ff_lt_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_bound. ff_lt_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_bound + S ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum = h) -> exists ff_a_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum ff_r_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum ff_s_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_summand. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_summand. etc_row_code_eft_fubini_total_universal_reduced_columns_witness_column_witness = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness) + (ff_a_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_partial. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_partial. ff_u_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) + (ff_r_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_successor. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_successor. ff_u_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) + (ff_s_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum))) /\ ff_s_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum = ff_r_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum + ff_a_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits. (exists ff_lt_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits_bound. ff_lt_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits_bound + S ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits = h) -> exists ff_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits_decoded. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits_decoded. etc_row_code_eft_fubini_total_universal_reduced_columns_witness_column_witness = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness) + (ff_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_inner_entry. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_inner_entry + S (etc_bit_eft_fubini_total_universal_reduced_columns_witness_column) = S ((S (eft_fixed_index_fubini_total_universal_reduced_columns)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_inner_entry. etc_row_code_eft_fubini_total_universal_reduced_columns_witness_column_witness = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_inner_entry * S ((S (eft_fixed_index_fubini_total_universal_reduced_columns)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness) + (etc_bit_eft_fubini_total_universal_reduced_columns_witness_column))))))) /\ (((exists ff_u_eft_fubini_total_universal_reduced_columns_witness_count_sum ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum. ((((exists ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_start. ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_start. ff_u_eft_fubini_total_universal_reduced_columns_witness_count_sum = ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_start * S ((S (0)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum) + (0))) /\ ((((exists ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_terminal. ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_terminal + S (eft_count_fubini_total_universal_reduced_columns) = S ((S (k)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_terminal. ff_u_eft_fubini_total_universal_reduced_columns_witness_count_sum = ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_terminal * S ((S (k)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum) + (eft_count_fubini_total_universal_reduced_columns))) /\ forall ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum. (exists ff_lt_eft_fubini_total_universal_reduced_columns_witness_count_sum_bound. ff_lt_eft_fubini_total_universal_reduced_columns_witness_count_sum_bound + S ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum = k) -> exists ff_a_eft_fubini_total_universal_reduced_columns_witness_count_sum ff_r_eft_fubini_total_universal_reduced_columns_witness_count_sum ff_s_eft_fubini_total_universal_reduced_columns_witness_count_sum. ((((exists ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_summand. ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_summand + S (ff_a_eft_fubini_total_universal_reduced_columns_witness_count_sum) = S ((S (ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum)) * eft_column_scale_fubini_total_universal_reduced_columns_witness)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_summand. eft_column_code_fubini_total_universal_reduced_columns_witness = ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_summand * S ((S (ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum)) * eft_column_scale_fubini_total_universal_reduced_columns_witness) + (ff_a_eft_fubini_total_universal_reduced_columns_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_partial. ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_partial + S (ff_r_eft_fubini_total_universal_reduced_columns_witness_count_sum) = S ((S (ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_partial. ff_u_eft_fubini_total_universal_reduced_columns_witness_count_sum = ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_partial * S ((S (ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum) + (ff_r_eft_fubini_total_universal_reduced_columns_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_successor. ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_successor + S (ff_s_eft_fubini_total_universal_reduced_columns_witness_count_sum) = S ((S (S ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_successor. ff_u_eft_fubini_total_universal_reduced_columns_witness_count_sum = ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_successor * S ((S (S ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum) + (ff_s_eft_fubini_total_universal_reduced_columns_witness_count_sum))) /\ ff_s_eft_fubini_total_universal_reduced_columns_witness_count_sum = ff_r_eft_fubini_total_universal_reduced_columns_witness_count_sum + ff_a_eft_fubini_total_universal_reduced_columns_witness_count_sum)))))) /\ (forall ff_i_eft_fubini_total_universal_reduced_columns_witness_count_bits. (exists ff_lt_eft_fubini_total_universal_reduced_columns_witness_count_bits_bound. ff_lt_eft_fubini_total_universal_reduced_columns_witness_count_bits_bound + S ff_i_eft_fubini_total_universal_reduced_columns_witness_count_bits = k) -> exists ff_bit_eft_fubini_total_universal_reduced_columns_witness_count_bits. ((((exists ff_h_eft_fubini_total_universal_reduced_columns_witness_count_bits_decoded. ff_h_eft_fubini_total_universal_reduced_columns_witness_count_bits_decoded + S (ff_bit_eft_fubini_total_universal_reduced_columns_witness_count_bits) = S ((S (ff_i_eft_fubini_total_universal_reduced_columns_witness_count_bits)) * eft_column_scale_fubini_total_universal_reduced_columns_witness)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_witness_count_bits_decoded. eft_column_code_fubini_total_universal_reduced_columns_witness = ff_q_eft_fubini_total_universal_reduced_columns_witness_count_bits_decoded * S ((S (ff_i_eft_fubini_total_universal_reduced_columns_witness_count_bits)) * eft_column_scale_fubini_total_universal_reduced_columns_witness) + (ff_bit_eft_fubini_total_universal_reduced_columns_witness_count_bits))) /\ (ff_bit_eft_fubini_total_universal_reduced_columns_witness_count_bits = 0 \/ ff_bit_eft_fubini_total_universal_reduced_columns_witness_count_bits = 1)))))))) - 0126
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor p - 0127
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor q - 0128
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor h - 0129
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor (S h) - 0130
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor bb - 0131
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor bc - 0132
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor x - 0133
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor x1 - 0134
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor db - 0135
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor dc - 0136
specialize eisenstein_fubini_column_count_prefix_retarget_predecessor k - 0137
apply eisenstein_fubini_column_count_prefix_retarget_predecessor - 0138
refl - 0139
exact hreduced_outer - 0140
exact hrestricted_columns - 0141
have hsum_decompose : ∃ a. ∃ r. BetaAt(db,dc,h,a) ∧ (Sum(db,dc,h,r) ∧ M = r + a)Exact native replay line
have hsum_decompose : exists a r. ((((exists ff_h_fubini_total_universal_column_last_entry. ff_h_fubini_total_universal_column_last_entry + S (a) = S ((S (h)) * dc)) /\ exists ff_q_fubini_total_universal_column_last_entry. db = ff_q_fubini_total_universal_column_last_entry * S ((S (h)) * dc) + (a))) /\ ((exists ff_u_fubini_total_universal_column_prefix_sum ff_v_fubini_total_universal_column_prefix_sum. ((((exists ff_h_fubini_total_universal_column_prefix_sum_start. ff_h_fubini_total_universal_column_prefix_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_universal_column_prefix_sum)) /\ exists ff_q_fubini_total_universal_column_prefix_sum_start. ff_u_fubini_total_universal_column_prefix_sum = ff_q_fubini_total_universal_column_prefix_sum_start * S ((S (0)) * ff_v_fubini_total_universal_column_prefix_sum) + (0))) /\ ((((exists ff_h_fubini_total_universal_column_prefix_sum_terminal. ff_h_fubini_total_universal_column_prefix_sum_terminal + S (r) = S ((S (h)) * ff_v_fubini_total_universal_column_prefix_sum)) /\ exists ff_q_fubini_total_universal_column_prefix_sum_terminal. ff_u_fubini_total_universal_column_prefix_sum = ff_q_fubini_total_universal_column_prefix_sum_terminal * S ((S (h)) * ff_v_fubini_total_universal_column_prefix_sum) + (r))) /\ forall ff_i_fubini_total_universal_column_prefix_sum. (exists ff_lt_fubini_total_universal_column_prefix_sum_bound. ff_lt_fubini_total_universal_column_prefix_sum_bound + S ff_i_fubini_total_universal_column_prefix_sum = h) -> exists ff_a_fubini_total_universal_column_prefix_sum ff_r_fubini_total_universal_column_prefix_sum ff_s_fubini_total_universal_column_prefix_sum. ((((exists ff_h_fubini_total_universal_column_prefix_sum_summand. ff_h_fubini_total_universal_column_prefix_sum_summand + S (ff_a_fubini_total_universal_column_prefix_sum) = S ((S (ff_i_fubini_total_universal_column_prefix_sum)) * dc)) /\ exists ff_q_fubini_total_universal_column_prefix_sum_summand. db = ff_q_fubini_total_universal_column_prefix_sum_summand * S ((S (ff_i_fubini_total_universal_column_prefix_sum)) * dc) + (ff_a_fubini_total_universal_column_prefix_sum))) /\ ((((exists ff_h_fubini_total_universal_column_prefix_sum_partial. ff_h_fubini_total_universal_column_prefix_sum_partial + S (ff_r_fubini_total_universal_column_prefix_sum) = S ((S (ff_i_fubini_total_universal_column_prefix_sum)) * ff_v_fubini_total_universal_column_prefix_sum)) /\ exists ff_q_fubini_total_universal_column_prefix_sum_partial. ff_u_fubini_total_universal_column_prefix_sum = ff_q_fubini_total_universal_column_prefix_sum_partial * S ((S (ff_i_fubini_total_universal_column_prefix_sum)) * ff_v_fubini_total_universal_column_prefix_sum) + (ff_r_fubini_total_universal_column_prefix_sum))) /\ ((((exists ff_h_fubini_total_universal_column_prefix_sum_successor. ff_h_fubini_total_universal_column_prefix_sum_successor + S (ff_s_fubini_total_universal_column_prefix_sum) = S ((S (S ff_i_fubini_total_universal_column_prefix_sum)) * ff_v_fubini_total_universal_column_prefix_sum)) /\ exists ff_q_fubini_total_universal_column_prefix_sum_successor. ff_u_fubini_total_universal_column_prefix_sum = ff_q_fubini_total_universal_column_prefix_sum_successor * S ((S (S ff_i_fubini_total_universal_column_prefix_sum)) * ff_v_fubini_total_universal_column_prefix_sum) + (ff_s_fubini_total_universal_column_prefix_sum))) /\ ff_s_fubini_total_universal_column_prefix_sum = ff_r_fubini_total_universal_column_prefix_sum + ff_a_fubini_total_universal_column_prefix_sum)))))) /\ M = r + a)) - 0142
specialize beta_sum_succ_decompose db - 0143
specialize beta_sum_succ_decompose dc - 0144
specialize beta_sum_succ_decompose h - 0145
specialize beta_sum_succ_decompose M - 0146
apply beta_sum_succ_decompose - 0147
exact hcolumnsum - 0148
cases hsum_decompose - 0149
cases hsum_decompose_witness - 0150
cases hsum_decompose_witness_witness - 0151
cases hsum_decompose_witness_witness_right - 0152
have hih : x7 = x4 - 0153
specialize IH p - 0154
specialize IH q - 0155
specialize IH k - 0156
specialize IH x - 0157
specialize IH x1 - 0158
specialize IH db - 0159
specialize IH dc - 0160
specialize IH x4 - 0161
specialize IH x7 - 0162
apply IH - 0163
exact hreduced_outer - 0164
exact hreduced_columns - 0165
exact hreduced_sum_witness - 0166
exact hsum_decompose_witness_witness_right_left - 0167
have hlast_stored : ∃ n. BetaAt(db,dc,h,n) ∧ (∃ x. ∃ y. (∀ z. Lt(z,k) → ∃ m. BetaAt(x,y,z,m) ∧ (∃ i. ∃ j. ∃ u. BetaAt(bb,bc,z,i) ∧ (∀ v. Lt(v,S h) → ∃ w. BetaAt(j,u,v,w) ∧ (w = 0 ∧ (Lt(p · S z,q · S v) ∧ ¬Lt(q · S v,p · S z)) ∨ w = 1 ∧ (Lt(q · S v,p · S z) ∧ ¬Lt(p · S z,q · S v)))) ∧ BitCount(j,u,S h,i) ∧ BetaAt(j,u,h,m))) ∧ BitCount(x,y,k,n))Exact native replay line
have hlast_stored : exists n. ((((exists ff_h_fubini_total_universal_last_stored_entry. ff_h_fubini_total_universal_last_stored_entry + S (n) = S ((S (h)) * dc)) /\ exists ff_q_fubini_total_universal_last_stored_entry. db = ff_q_fubini_total_universal_last_stored_entry * S ((S (h)) * dc) + (n))) /\ (exists eft_column_code_fubini_total_universal_last_stored_witness eft_column_scale_fubini_total_universal_last_stored_witness. ((forall etc_row_index_eft_fubini_total_universal_last_stored_witness_column. (exists edt_lt_gap_eft_fubini_total_universal_last_stored_witness_column_bound. edt_lt_gap_eft_fubini_total_universal_last_stored_witness_column_bound + S (etc_row_index_eft_fubini_total_universal_last_stored_witness_column) = k) -> exists etc_bit_eft_fubini_total_universal_last_stored_witness_column. ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_decoded. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_decoded + S (etc_bit_eft_fubini_total_universal_last_stored_witness_column) = S ((S (etc_row_index_eft_fubini_total_universal_last_stored_witness_column)) * eft_column_scale_fubini_total_universal_last_stored_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_decoded. eft_column_code_fubini_total_universal_last_stored_witness = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_decoded * S ((S (etc_row_index_eft_fubini_total_universal_last_stored_witness_column)) * eft_column_scale_fubini_total_universal_last_stored_witness) + (etc_bit_eft_fubini_total_universal_last_stored_witness_column))) /\ (exists etc_count_eft_fubini_total_universal_last_stored_witness_column_witness etc_row_code_eft_fubini_total_universal_last_stored_witness_column_witness etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness. ((((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_outer_entry. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_outer_entry + S (etc_count_eft_fubini_total_universal_last_stored_witness_column_witness) = S ((S (etc_row_index_eft_fubini_total_universal_last_stored_witness_column)) * bc)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_outer_entry. bb = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_outer_entry * S ((S (etc_row_index_eft_fubini_total_universal_last_stored_witness_column)) * bc) + (etc_count_eft_fubini_total_universal_last_stored_witness_column_witness))) /\ (forall eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row. (exists eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_bound. eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_bound + S (eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row) = S h) -> exists eri_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row. ((((exists ff_h_eri_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_decoded. ff_h_eri_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_decoded + S (eri_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row) = S ((S (eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness)) /\ exists ff_q_eri_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_decoded. etc_row_code_eft_fubini_total_universal_last_stored_witness_column_witness = ff_q_eri_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_decoded * S ((S (eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness) + (eri_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row))) /\ (((eri_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_universal_last_stored_witness_column) = q * S eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row) /\ ~(exists eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_universal_last_stored_witness_column))) \/ (eri_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_universal_last_stored_witness_column) /\ ~(exists eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_universal_last_stored_witness_column) = q * S eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_start. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_start. ff_u_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_terminal. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_terminal + S (etc_count_eft_fubini_total_universal_last_stored_witness_column_witness) = S ((S (S h)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_terminal. ff_u_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_terminal * S ((S (S h)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) + (etc_count_eft_fubini_total_universal_last_stored_witness_column_witness))) /\ forall ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum. (exists ff_lt_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_bound. ff_lt_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_bound + S ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum = S h) -> exists ff_a_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum ff_r_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum ff_s_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_summand. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_summand. etc_row_code_eft_fubini_total_universal_last_stored_witness_column_witness = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness) + (ff_a_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_partial. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_partial. ff_u_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) + (ff_r_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_successor. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_successor. ff_u_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) + (ff_s_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum))) /\ ff_s_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum = ff_r_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum + ff_a_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits. (exists ff_lt_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits_bound. ff_lt_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits_bound + S ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits = S h) -> exists ff_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits_decoded. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits_decoded. etc_row_code_eft_fubini_total_universal_last_stored_witness_column_witness = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness) + (ff_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_inner_entry. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_inner_entry + S (etc_bit_eft_fubini_total_universal_last_stored_witness_column) = S ((S (h)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_inner_entry. etc_row_code_eft_fubini_total_universal_last_stored_witness_column_witness = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_inner_entry * S ((S (h)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness) + (etc_bit_eft_fubini_total_universal_last_stored_witness_column))))))) /\ (((exists ff_u_eft_fubini_total_universal_last_stored_witness_count_sum ff_v_eft_fubini_total_universal_last_stored_witness_count_sum. ((((exists ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_start. ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_start. ff_u_eft_fubini_total_universal_last_stored_witness_count_sum = ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_start * S ((S (0)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum) + (0))) /\ ((((exists ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_terminal. ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_terminal + S (n) = S ((S (k)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_terminal. ff_u_eft_fubini_total_universal_last_stored_witness_count_sum = ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_terminal * S ((S (k)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum) + (n))) /\ forall ff_i_eft_fubini_total_universal_last_stored_witness_count_sum. (exists ff_lt_eft_fubini_total_universal_last_stored_witness_count_sum_bound. ff_lt_eft_fubini_total_universal_last_stored_witness_count_sum_bound + S ff_i_eft_fubini_total_universal_last_stored_witness_count_sum = k) -> exists ff_a_eft_fubini_total_universal_last_stored_witness_count_sum ff_r_eft_fubini_total_universal_last_stored_witness_count_sum ff_s_eft_fubini_total_universal_last_stored_witness_count_sum. ((((exists ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_summand. ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_summand + S (ff_a_eft_fubini_total_universal_last_stored_witness_count_sum) = S ((S (ff_i_eft_fubini_total_universal_last_stored_witness_count_sum)) * eft_column_scale_fubini_total_universal_last_stored_witness)) /\ exists ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_summand. eft_column_code_fubini_total_universal_last_stored_witness = ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_summand * S ((S (ff_i_eft_fubini_total_universal_last_stored_witness_count_sum)) * eft_column_scale_fubini_total_universal_last_stored_witness) + (ff_a_eft_fubini_total_universal_last_stored_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_partial. ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_partial + S (ff_r_eft_fubini_total_universal_last_stored_witness_count_sum) = S ((S (ff_i_eft_fubini_total_universal_last_stored_witness_count_sum)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_partial. ff_u_eft_fubini_total_universal_last_stored_witness_count_sum = ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_partial * S ((S (ff_i_eft_fubini_total_universal_last_stored_witness_count_sum)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum) + (ff_r_eft_fubini_total_universal_last_stored_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_successor. ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_successor + S (ff_s_eft_fubini_total_universal_last_stored_witness_count_sum) = S ((S (S ff_i_eft_fubini_total_universal_last_stored_witness_count_sum)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_successor. ff_u_eft_fubini_total_universal_last_stored_witness_count_sum = ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_successor * S ((S (S ff_i_eft_fubini_total_universal_last_stored_witness_count_sum)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum) + (ff_s_eft_fubini_total_universal_last_stored_witness_count_sum))) /\ ff_s_eft_fubini_total_universal_last_stored_witness_count_sum = ff_r_eft_fubini_total_universal_last_stored_witness_count_sum + ff_a_eft_fubini_total_universal_last_stored_witness_count_sum)))))) /\ (forall ff_i_eft_fubini_total_universal_last_stored_witness_count_bits. (exists ff_lt_eft_fubini_total_universal_last_stored_witness_count_bits_bound. ff_lt_eft_fubini_total_universal_last_stored_witness_count_bits_bound + S ff_i_eft_fubini_total_universal_last_stored_witness_count_bits = k) -> exists ff_bit_eft_fubini_total_universal_last_stored_witness_count_bits. ((((exists ff_h_eft_fubini_total_universal_last_stored_witness_count_bits_decoded. ff_h_eft_fubini_total_universal_last_stored_witness_count_bits_decoded + S (ff_bit_eft_fubini_total_universal_last_stored_witness_count_bits) = S ((S (ff_i_eft_fubini_total_universal_last_stored_witness_count_bits)) * eft_column_scale_fubini_total_universal_last_stored_witness)) /\ exists ff_q_eft_fubini_total_universal_last_stored_witness_count_bits_decoded. eft_column_code_fubini_total_universal_last_stored_witness = ff_q_eft_fubini_total_universal_last_stored_witness_count_bits_decoded * S ((S (ff_i_eft_fubini_total_universal_last_stored_witness_count_bits)) * eft_column_scale_fubini_total_universal_last_stored_witness) + (ff_bit_eft_fubini_total_universal_last_stored_witness_count_bits))) /\ (ff_bit_eft_fubini_total_universal_last_stored_witness_count_bits = 0 \/ ff_bit_eft_fubini_total_universal_last_stored_witness_count_bits = 1)))))))) - 0168
specialize hcolumns h - 0169
apply hcolumns - 0170
specialize le_refl (S h) - 0171
exact le_refl - 0172
cases hlast_stored - 0173
cases hlast_stored_witness - 0174
cases hlast_stored_witness_right - 0175
cases hlast_stored_witness_right_witness - 0176
cases hlast_stored_witness_right_witness_witness - 0177
cases hlast_stored_witness_right_witness_witness_right - 0178
have hcount_eq : x8 = x6 - 0179
specialize beta_at_unique db - 0180
specialize beta_at_unique dc - 0181
specialize beta_at_unique h - 0182
specialize beta_at_unique x8 - 0183
specialize beta_at_unique x6 - 0184
apply beta_at_unique - 0185
exact hlast_stored_witness_left - 0186
exact hsum_decompose_witness_witness_left - 0187
have hterminal_eq : x5 = x8 - 0188
specialize eisenstein_successor_terminal_sum_matches_last_column p - 0189
specialize eisenstein_successor_terminal_sum_matches_last_column q - 0190
specialize eisenstein_successor_terminal_sum_matches_last_column h - 0191
specialize eisenstein_successor_terminal_sum_matches_last_column (S h) - 0192
specialize eisenstein_successor_terminal_sum_matches_last_column bb - 0193
specialize eisenstein_successor_terminal_sum_matches_last_column bc - 0194
specialize eisenstein_successor_terminal_sum_matches_last_column x - 0195
specialize eisenstein_successor_terminal_sum_matches_last_column x1 - 0196
specialize eisenstein_successor_terminal_sum_matches_last_column x2 - 0197
specialize eisenstein_successor_terminal_sum_matches_last_column x3 - 0198
specialize eisenstein_successor_terminal_sum_matches_last_column x9 - 0199
specialize eisenstein_successor_terminal_sum_matches_last_column x10 - 0200
specialize eisenstein_successor_terminal_sum_matches_last_column k - 0201
specialize eisenstein_successor_terminal_sum_matches_last_column x5 - 0202
specialize eisenstein_successor_terminal_sum_matches_last_column x8 - 0203
apply eisenstein_successor_terminal_sum_matches_last_column - 0204
refl - 0205
exact hsplit_exists_witness_witness_witness_witness - 0206
exact hlast_stored_witness_right_witness_witness_left - 0207
exact hterminal_sum_witness - 0208
exact hlast_stored_witness_right_witness_witness_right_left - 0209
have htotal : M = x4 + x5 - 0210
rewrite hih at hsum_decompose_witness_witness_right_right - 0211
rewrite <- hcount_eq at hsum_decompose_witness_witness_right_right - 0212
rewrite <- hterminal_eq at hsum_decompose_witness_witness_right_right - 0213
exact hsum_decompose_witness_witness_right_right - 0214
trans x4 + x5 - 0215
exact htotal - 0216
exact hsource_add