PA00FE · theorem

eisenstein_rectangle_floor_sum_identity

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

The two semantic Eisenstein row totals add exactly to the rectangle area.

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

Statement with defined notation

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

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0015 Sum PD0017 BitCount

20 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0015 Sum PD0017 BitCount

23 occurrences

Exact expanded native-PA statement
forall p q h k ab ac bb bc N T. (forall erc_row_fubini_total_identity_first_outer. (exists erc_lt_gap_fubini_total_identity_first_outer_bound. erc_lt_gap_fubini_total_identity_first_outer_bound + S (erc_row_fubini_total_identity_first_outer) = h) -> exists erc_count_fubini_total_identity_first_outer. ((((exists ff_h_erc_fubini_total_identity_first_outer_decoded. ff_h_erc_fubini_total_identity_first_outer_decoded + S (erc_count_fubini_total_identity_first_outer) = S ((S (erc_row_fubini_total_identity_first_outer)) * ac)) /\ exists ff_q_erc_fubini_total_identity_first_outer_decoded. ab = ff_q_erc_fubini_total_identity_first_outer_decoded * S ((S (erc_row_fubini_total_identity_first_outer)) * ac) + (erc_count_fubini_total_identity_first_outer))) /\ (exists erc_row_code_fubini_total_identity_first_outer_witness erc_row_scale_fubini_total_identity_first_outer_witness. ((forall eri_column_erc_fubini_total_identity_first_outer_witness_row. (exists eri_gap_erc_fubini_total_identity_first_outer_witness_row_bound. eri_gap_erc_fubini_total_identity_first_outer_witness_row_bound + S (eri_column_erc_fubini_total_identity_first_outer_witness_row) = k) -> exists eri_bit_erc_fubini_total_identity_first_outer_witness_row. ((((exists ff_h_eri_erc_fubini_total_identity_first_outer_witness_row_decoded. ff_h_eri_erc_fubini_total_identity_first_outer_witness_row_decoded + S (eri_bit_erc_fubini_total_identity_first_outer_witness_row) = S ((S (eri_column_erc_fubini_total_identity_first_outer_witness_row)) * erc_row_scale_fubini_total_identity_first_outer_witness)) /\ exists ff_q_eri_erc_fubini_total_identity_first_outer_witness_row_decoded. erc_row_code_fubini_total_identity_first_outer_witness = ff_q_eri_erc_fubini_total_identity_first_outer_witness_row_decoded * S ((S (eri_column_erc_fubini_total_identity_first_outer_witness_row)) * erc_row_scale_fubini_total_identity_first_outer_witness) + (eri_bit_erc_fubini_total_identity_first_outer_witness_row))) /\ (((eri_bit_erc_fubini_total_identity_first_outer_witness_row = 0 /\ ((exists eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_left. eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_left + S (q * S erc_row_fubini_total_identity_first_outer) = p * S eri_column_erc_fubini_total_identity_first_outer_witness_row) /\ ~(exists eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_right. eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_right + S (p * S eri_column_erc_fubini_total_identity_first_outer_witness_row) = q * S erc_row_fubini_total_identity_first_outer))) \/ (eri_bit_erc_fubini_total_identity_first_outer_witness_row = 1 /\ ((exists eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_right. eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_right + S (p * S eri_column_erc_fubini_total_identity_first_outer_witness_row) = q * S erc_row_fubini_total_identity_first_outer) /\ ~(exists eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_left. eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_left + S (q * S erc_row_fubini_total_identity_first_outer) = p * S eri_column_erc_fubini_total_identity_first_outer_witness_row))))))) /\ (((exists ff_u_erc_fubini_total_identity_first_outer_witness_count_sum ff_v_erc_fubini_total_identity_first_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_start. ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_start. ff_u_erc_fubini_total_identity_first_outer_witness_count_sum = ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_terminal. ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_terminal + S (erc_count_fubini_total_identity_first_outer) = S ((S (k)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_terminal. ff_u_erc_fubini_total_identity_first_outer_witness_count_sum = ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum) + (erc_count_fubini_total_identity_first_outer))) /\ forall ff_i_erc_fubini_total_identity_first_outer_witness_count_sum. (exists ff_lt_erc_fubini_total_identity_first_outer_witness_count_sum_bound. ff_lt_erc_fubini_total_identity_first_outer_witness_count_sum_bound + S ff_i_erc_fubini_total_identity_first_outer_witness_count_sum = k) -> exists ff_a_erc_fubini_total_identity_first_outer_witness_count_sum ff_r_erc_fubini_total_identity_first_outer_witness_count_sum ff_s_erc_fubini_total_identity_first_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_summand. ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_summand + S (ff_a_erc_fubini_total_identity_first_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_identity_first_outer_witness_count_sum)) * erc_row_scale_fubini_total_identity_first_outer_witness)) /\ exists ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_summand. erc_row_code_fubini_total_identity_first_outer_witness = ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_summand * S ((S (ff_i_erc_fubini_total_identity_first_outer_witness_count_sum)) * erc_row_scale_fubini_total_identity_first_outer_witness) + (ff_a_erc_fubini_total_identity_first_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_partial. ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_partial + S (ff_r_erc_fubini_total_identity_first_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_identity_first_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_partial. ff_u_erc_fubini_total_identity_first_outer_witness_count_sum = ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_partial * S ((S (ff_i_erc_fubini_total_identity_first_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum) + (ff_r_erc_fubini_total_identity_first_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_successor. ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_successor + S (ff_s_erc_fubini_total_identity_first_outer_witness_count_sum) = S ((S (S ff_i_erc_fubini_total_identity_first_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_successor. ff_u_erc_fubini_total_identity_first_outer_witness_count_sum = ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_total_identity_first_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum) + (ff_s_erc_fubini_total_identity_first_outer_witness_count_sum))) /\ ff_s_erc_fubini_total_identity_first_outer_witness_count_sum = ff_r_erc_fubini_total_identity_first_outer_witness_count_sum + ff_a_erc_fubini_total_identity_first_outer_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_total_identity_first_outer_witness_count_bits. (exists ff_lt_erc_fubini_total_identity_first_outer_witness_count_bits_bound. ff_lt_erc_fubini_total_identity_first_outer_witness_count_bits_bound + S ff_i_erc_fubini_total_identity_first_outer_witness_count_bits = k) -> exists ff_bit_erc_fubini_total_identity_first_outer_witness_count_bits. ((((exists ff_h_erc_fubini_total_identity_first_outer_witness_count_bits_decoded. ff_h_erc_fubini_total_identity_first_outer_witness_count_bits_decoded + S (ff_bit_erc_fubini_total_identity_first_outer_witness_count_bits) = S ((S (ff_i_erc_fubini_total_identity_first_outer_witness_count_bits)) * erc_row_scale_fubini_total_identity_first_outer_witness)) /\ exists ff_q_erc_fubini_total_identity_first_outer_witness_count_bits_decoded. erc_row_code_fubini_total_identity_first_outer_witness = ff_q_erc_fubini_total_identity_first_outer_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_total_identity_first_outer_witness_count_bits)) * erc_row_scale_fubini_total_identity_first_outer_witness) + (ff_bit_erc_fubini_total_identity_first_outer_witness_count_bits))) /\ (ff_bit_erc_fubini_total_identity_first_outer_witness_count_bits = 0 \/ ff_bit_erc_fubini_total_identity_first_outer_witness_count_bits = 1))))))))) -> (forall erc_row_fubini_total_identity_second_outer. (exists erc_lt_gap_fubini_total_identity_second_outer_bound. erc_lt_gap_fubini_total_identity_second_outer_bound + S (erc_row_fubini_total_identity_second_outer) = k) -> exists erc_count_fubini_total_identity_second_outer. ((((exists ff_h_erc_fubini_total_identity_second_outer_decoded. ff_h_erc_fubini_total_identity_second_outer_decoded + S (erc_count_fubini_total_identity_second_outer) = S ((S (erc_row_fubini_total_identity_second_outer)) * bc)) /\ exists ff_q_erc_fubini_total_identity_second_outer_decoded. bb = ff_q_erc_fubini_total_identity_second_outer_decoded * S ((S (erc_row_fubini_total_identity_second_outer)) * bc) + (erc_count_fubini_total_identity_second_outer))) /\ (exists erc_row_code_fubini_total_identity_second_outer_witness erc_row_scale_fubini_total_identity_second_outer_witness. ((forall eri_column_erc_fubini_total_identity_second_outer_witness_row. (exists eri_gap_erc_fubini_total_identity_second_outer_witness_row_bound. eri_gap_erc_fubini_total_identity_second_outer_witness_row_bound + S (eri_column_erc_fubini_total_identity_second_outer_witness_row) = h) -> exists eri_bit_erc_fubini_total_identity_second_outer_witness_row. ((((exists ff_h_eri_erc_fubini_total_identity_second_outer_witness_row_decoded. ff_h_eri_erc_fubini_total_identity_second_outer_witness_row_decoded + S (eri_bit_erc_fubini_total_identity_second_outer_witness_row) = S ((S (eri_column_erc_fubini_total_identity_second_outer_witness_row)) * erc_row_scale_fubini_total_identity_second_outer_witness)) /\ exists ff_q_eri_erc_fubini_total_identity_second_outer_witness_row_decoded. erc_row_code_fubini_total_identity_second_outer_witness = ff_q_eri_erc_fubini_total_identity_second_outer_witness_row_decoded * S ((S (eri_column_erc_fubini_total_identity_second_outer_witness_row)) * erc_row_scale_fubini_total_identity_second_outer_witness) + (eri_bit_erc_fubini_total_identity_second_outer_witness_row))) /\ (((eri_bit_erc_fubini_total_identity_second_outer_witness_row = 0 /\ ((exists eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_left. eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_identity_second_outer) = q * S eri_column_erc_fubini_total_identity_second_outer_witness_row) /\ ~(exists eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_right. eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_identity_second_outer_witness_row) = p * S erc_row_fubini_total_identity_second_outer))) \/ (eri_bit_erc_fubini_total_identity_second_outer_witness_row = 1 /\ ((exists eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_right. eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_identity_second_outer_witness_row) = p * S erc_row_fubini_total_identity_second_outer) /\ ~(exists eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_left. eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_identity_second_outer) = q * S eri_column_erc_fubini_total_identity_second_outer_witness_row))))))) /\ (((exists ff_u_erc_fubini_total_identity_second_outer_witness_count_sum ff_v_erc_fubini_total_identity_second_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_start. ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_start. ff_u_erc_fubini_total_identity_second_outer_witness_count_sum = ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_terminal. ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_terminal + S (erc_count_fubini_total_identity_second_outer) = S ((S (h)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_terminal. ff_u_erc_fubini_total_identity_second_outer_witness_count_sum = ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_terminal * S ((S (h)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum) + (erc_count_fubini_total_identity_second_outer))) /\ forall ff_i_erc_fubini_total_identity_second_outer_witness_count_sum. (exists ff_lt_erc_fubini_total_identity_second_outer_witness_count_sum_bound. ff_lt_erc_fubini_total_identity_second_outer_witness_count_sum_bound + S ff_i_erc_fubini_total_identity_second_outer_witness_count_sum = h) -> exists ff_a_erc_fubini_total_identity_second_outer_witness_count_sum ff_r_erc_fubini_total_identity_second_outer_witness_count_sum ff_s_erc_fubini_total_identity_second_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_summand. ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_summand + S (ff_a_erc_fubini_total_identity_second_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_identity_second_outer_witness_count_sum)) * erc_row_scale_fubini_total_identity_second_outer_witness)) /\ exists ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_summand. erc_row_code_fubini_total_identity_second_outer_witness = ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_summand * S ((S (ff_i_erc_fubini_total_identity_second_outer_witness_count_sum)) * erc_row_scale_fubini_total_identity_second_outer_witness) + (ff_a_erc_fubini_total_identity_second_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_partial. ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_partial + S (ff_r_erc_fubini_total_identity_second_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_identity_second_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_partial. ff_u_erc_fubini_total_identity_second_outer_witness_count_sum = ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_partial * S ((S (ff_i_erc_fubini_total_identity_second_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum) + (ff_r_erc_fubini_total_identity_second_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_successor. ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_successor + S (ff_s_erc_fubini_total_identity_second_outer_witness_count_sum) = S ((S (S ff_i_erc_fubini_total_identity_second_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_successor. ff_u_erc_fubini_total_identity_second_outer_witness_count_sum = ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_total_identity_second_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum) + (ff_s_erc_fubini_total_identity_second_outer_witness_count_sum))) /\ ff_s_erc_fubini_total_identity_second_outer_witness_count_sum = ff_r_erc_fubini_total_identity_second_outer_witness_count_sum + ff_a_erc_fubini_total_identity_second_outer_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_total_identity_second_outer_witness_count_bits. (exists ff_lt_erc_fubini_total_identity_second_outer_witness_count_bits_bound. ff_lt_erc_fubini_total_identity_second_outer_witness_count_bits_bound + S ff_i_erc_fubini_total_identity_second_outer_witness_count_bits = h) -> exists ff_bit_erc_fubini_total_identity_second_outer_witness_count_bits. ((((exists ff_h_erc_fubini_total_identity_second_outer_witness_count_bits_decoded. ff_h_erc_fubini_total_identity_second_outer_witness_count_bits_decoded + S (ff_bit_erc_fubini_total_identity_second_outer_witness_count_bits) = S ((S (ff_i_erc_fubini_total_identity_second_outer_witness_count_bits)) * erc_row_scale_fubini_total_identity_second_outer_witness)) /\ exists ff_q_erc_fubini_total_identity_second_outer_witness_count_bits_decoded. erc_row_code_fubini_total_identity_second_outer_witness = ff_q_erc_fubini_total_identity_second_outer_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_total_identity_second_outer_witness_count_bits)) * erc_row_scale_fubini_total_identity_second_outer_witness) + (ff_bit_erc_fubini_total_identity_second_outer_witness_count_bits))) /\ (ff_bit_erc_fubini_total_identity_second_outer_witness_count_bits = 0 \/ ff_bit_erc_fubini_total_identity_second_outer_witness_count_bits = 1))))))))) -> (exists ff_u_fubini_total_identity_first_sum ff_v_fubini_total_identity_first_sum. ((((exists ff_h_fubini_total_identity_first_sum_start. ff_h_fubini_total_identity_first_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_identity_first_sum)) /\ exists ff_q_fubini_total_identity_first_sum_start. ff_u_fubini_total_identity_first_sum = ff_q_fubini_total_identity_first_sum_start * S ((S (0)) * ff_v_fubini_total_identity_first_sum) + (0))) /\ ((((exists ff_h_fubini_total_identity_first_sum_terminal. ff_h_fubini_total_identity_first_sum_terminal + S (N) = S ((S (h)) * ff_v_fubini_total_identity_first_sum)) /\ exists ff_q_fubini_total_identity_first_sum_terminal. ff_u_fubini_total_identity_first_sum = ff_q_fubini_total_identity_first_sum_terminal * S ((S (h)) * ff_v_fubini_total_identity_first_sum) + (N))) /\ forall ff_i_fubini_total_identity_first_sum. (exists ff_lt_fubini_total_identity_first_sum_bound. ff_lt_fubini_total_identity_first_sum_bound + S ff_i_fubini_total_identity_first_sum = h) -> exists ff_a_fubini_total_identity_first_sum ff_r_fubini_total_identity_first_sum ff_s_fubini_total_identity_first_sum. ((((exists ff_h_fubini_total_identity_first_sum_summand. ff_h_fubini_total_identity_first_sum_summand + S (ff_a_fubini_total_identity_first_sum) = S ((S (ff_i_fubini_total_identity_first_sum)) * ac)) /\ exists ff_q_fubini_total_identity_first_sum_summand. ab = ff_q_fubini_total_identity_first_sum_summand * S ((S (ff_i_fubini_total_identity_first_sum)) * ac) + (ff_a_fubini_total_identity_first_sum))) /\ ((((exists ff_h_fubini_total_identity_first_sum_partial. ff_h_fubini_total_identity_first_sum_partial + S (ff_r_fubini_total_identity_first_sum) = S ((S (ff_i_fubini_total_identity_first_sum)) * ff_v_fubini_total_identity_first_sum)) /\ exists ff_q_fubini_total_identity_first_sum_partial. ff_u_fubini_total_identity_first_sum = ff_q_fubini_total_identity_first_sum_partial * S ((S (ff_i_fubini_total_identity_first_sum)) * ff_v_fubini_total_identity_first_sum) + (ff_r_fubini_total_identity_first_sum))) /\ ((((exists ff_h_fubini_total_identity_first_sum_successor. ff_h_fubini_total_identity_first_sum_successor + S (ff_s_fubini_total_identity_first_sum) = S ((S (S ff_i_fubini_total_identity_first_sum)) * ff_v_fubini_total_identity_first_sum)) /\ exists ff_q_fubini_total_identity_first_sum_successor. ff_u_fubini_total_identity_first_sum = ff_q_fubini_total_identity_first_sum_successor * S ((S (S ff_i_fubini_total_identity_first_sum)) * ff_v_fubini_total_identity_first_sum) + (ff_s_fubini_total_identity_first_sum))) /\ ff_s_fubini_total_identity_first_sum = ff_r_fubini_total_identity_first_sum + ff_a_fubini_total_identity_first_sum)))))) -> (exists ff_u_fubini_total_identity_second_sum ff_v_fubini_total_identity_second_sum. ((((exists ff_h_fubini_total_identity_second_sum_start. ff_h_fubini_total_identity_second_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_identity_second_sum)) /\ exists ff_q_fubini_total_identity_second_sum_start. ff_u_fubini_total_identity_second_sum = ff_q_fubini_total_identity_second_sum_start * S ((S (0)) * ff_v_fubini_total_identity_second_sum) + (0))) /\ ((((exists ff_h_fubini_total_identity_second_sum_terminal. ff_h_fubini_total_identity_second_sum_terminal + S (T) = S ((S (k)) * ff_v_fubini_total_identity_second_sum)) /\ exists ff_q_fubini_total_identity_second_sum_terminal. ff_u_fubini_total_identity_second_sum = ff_q_fubini_total_identity_second_sum_terminal * S ((S (k)) * ff_v_fubini_total_identity_second_sum) + (T))) /\ forall ff_i_fubini_total_identity_second_sum. (exists ff_lt_fubini_total_identity_second_sum_bound. ff_lt_fubini_total_identity_second_sum_bound + S ff_i_fubini_total_identity_second_sum = k) -> exists ff_a_fubini_total_identity_second_sum ff_r_fubini_total_identity_second_sum ff_s_fubini_total_identity_second_sum. ((((exists ff_h_fubini_total_identity_second_sum_summand. ff_h_fubini_total_identity_second_sum_summand + S (ff_a_fubini_total_identity_second_sum) = S ((S (ff_i_fubini_total_identity_second_sum)) * bc)) /\ exists ff_q_fubini_total_identity_second_sum_summand. bb = ff_q_fubini_total_identity_second_sum_summand * S ((S (ff_i_fubini_total_identity_second_sum)) * bc) + (ff_a_fubini_total_identity_second_sum))) /\ ((((exists ff_h_fubini_total_identity_second_sum_partial. ff_h_fubini_total_identity_second_sum_partial + S (ff_r_fubini_total_identity_second_sum) = S ((S (ff_i_fubini_total_identity_second_sum)) * ff_v_fubini_total_identity_second_sum)) /\ exists ff_q_fubini_total_identity_second_sum_partial. ff_u_fubini_total_identity_second_sum = ff_q_fubini_total_identity_second_sum_partial * S ((S (ff_i_fubini_total_identity_second_sum)) * ff_v_fubini_total_identity_second_sum) + (ff_r_fubini_total_identity_second_sum))) /\ ((((exists ff_h_fubini_total_identity_second_sum_successor. ff_h_fubini_total_identity_second_sum_successor + S (ff_s_fubini_total_identity_second_sum) = S ((S (S ff_i_fubini_total_identity_second_sum)) * ff_v_fubini_total_identity_second_sum)) /\ exists ff_q_fubini_total_identity_second_sum_successor. ff_u_fubini_total_identity_second_sum = ff_q_fubini_total_identity_second_sum_successor * S ((S (S ff_i_fubini_total_identity_second_sum)) * ff_v_fubini_total_identity_second_sum) + (ff_s_fubini_total_identity_second_sum))) /\ ff_s_fubini_total_identity_second_sum = ff_r_fubini_total_identity_second_sum + ff_a_fubini_total_identity_second_sum)))))) -> N + T = h * k

Proof neighborhood

Direct theorem prerequisites

PA00EQ eisenstein_rectangle_plus_column_count_total PA00FD eisenstein_constructed_column_total_equals_swapped_total

Direct theorem dependents

PA00FF distinct_odd_prime_eisenstein_quotient_sum_identity

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

53 script commands · 9 reading checkpoints · 2 local claims

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

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

Named ingredients (2)
eisenstein rectangle plus column count totaleisenstein constructed column total equals swapped total
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro h
  4. L4
    intro k
  5. L5
    intro ab
  6. L6
    intro ac
  7. L7
    intro bb
  8. L8
    intro bc
  9. L9
    intro N
  10. L10
    intro T
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hfirst
  2. L12
    intro hsecond
  3. L13
    intro hfirstsum
  4. L14
    intro hsecondsum
03Establish hpartitionL15–24

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

  1. L15
    have hpartition · expand full local formula (642 characters)have hpartition : ∃ db. ∃ dc. ∃ M. (∀ x. Lt(x,h) → ∃ y. BetaAt(db,dc,x,y) ∧ (∃ z. ∃ n. ∃ m. BetaAt(ab,ac,x,z) ∧ (∃ i. ∃ j. (∀ u. Lt(u,k) → ∃ v. BetaAt(i,j,u,v) ∧ (v = 0 ∧ (Lt(q · S x,p · S u) ∧ ¬Lt(p · S u,q · S x)) ∨ v = 1 ∧ (Lt(p · S u,q · S x) ∧ ¬Lt(q · S x,p · S u)))) ∧ BitCount(i,j,k,z)) ∧ (∀ i. Lt(i,k) → ∃ j. BetaAt(n,m,i,j) ∧ (∃ u. ∃ v. ∃ w. BetaAt(bb,bc,i,u) ∧ (∀ x0. Lt(x0,h) → ∃ x1. BetaAt(v,w,x0,x1) ∧ (x1 = 0 ∧ (Lt(p · S i,q · S x0) ∧ ¬Lt(q · S x0,p · S i)) ∨ x1 = 1 ∧ (Lt(q · S x0,p · S i) ∧ ¬Lt(p · S i,q · S x0)))) ∧ BitCount(v,w,h,u) ∧ BetaAt(v,w,x,j))) ∧ (BitCount(n,m,k,y) ∧ z + y = k))) ∧ (Sum(db,dc,h,M) ∧ N + M = h · k)
    Definitions: Lt(x,h)BetaAt(db,dc,x,y)BetaAt(ab,ac,x,z)Lt(u,k)BetaAt(i,j,u,v)Lt(q · S x,p · S u)Lt(p · S u,q · S x)BitCount(i,j,k,z)Lt(i,k)BetaAt(n,m,i,j)BetaAt(bb,bc,i,u)Lt(x0,h)BetaAt(v,w,x0,x1)Lt(p · S i,q · S x0)Lt(q · S x0,p · S i)BitCount(v,w,h,u)BetaAt(v,w,x,j)BitCount(n,m,k,y)Sum(db,dc,h,M)Original native command in the exact edition
  2. L16
    specialize eisenstein_rectangle_plus_column_count_total p
  3. L17
    specialize eisenstein_rectangle_plus_column_count_total q
  4. L18
    specialize eisenstein_rectangle_plus_column_count_total h
  5. L19
    specialize eisenstein_rectangle_plus_column_count_total k
  6. L20
    specialize eisenstein_rectangle_plus_column_count_total ab
  7. L21
    specialize eisenstein_rectangle_plus_column_count_total ac
  8. L22
    specialize eisenstein_rectangle_plus_column_count_total bb
  9. L23
    specialize eisenstein_rectangle_plus_column_count_total bc
  10. L24
    specialize eisenstein_rectangle_plus_column_count_total N
04Use earlier factsL25–28

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

  1. L25
    apply eisenstein_rectangle_plus_column_count_total
  2. L26
    exact hfirst
  3. L27
    exact hsecond
  4. L28
    exact hfirstsum
05Separate the logical casesL29–33

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

  1. L29
    cases hpartition
  2. L30
    cases hpartition_witness
  3. L31
    cases hpartition_witness_witness
  4. L32
    cases hpartition_witness_witness_witness
  5. L33
    cases hpartition_witness_witness_witness_right
06Establish heqL34–43

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

  1. L34
    have heq : x2 = T
  2. L35
    specialize eisenstein_constructed_column_total_equals_swapped_total p
  3. L36
    specialize eisenstein_constructed_column_total_equals_swapped_total q
  4. L37
    specialize eisenstein_constructed_column_total_equals_swapped_total h
  5. L38
    specialize eisenstein_constructed_column_total_equals_swapped_total k
  6. L39
    specialize eisenstein_constructed_column_total_equals_swapped_total ab
  7. L40
    specialize eisenstein_constructed_column_total_equals_swapped_total ac
  8. L41
    specialize eisenstein_constructed_column_total_equals_swapped_total bb
  9. L42
    specialize eisenstein_constructed_column_total_equals_swapped_total bc
  10. L43
    specialize eisenstein_constructed_column_total_equals_swapped_total x
07Use earlier factsL44–51

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

  1. L44
    specialize eisenstein_constructed_column_total_equals_swapped_total x1
  2. L45
    specialize eisenstein_constructed_column_total_equals_swapped_total T
  3. L46
    specialize eisenstein_constructed_column_total_equals_swapped_total x2
  4. L47
    apply eisenstein_constructed_column_total_equals_swapped_total
  5. L48
    exact hsecond
  6. L49
    exact hpartition_witness_witness_witness_left
  7. L50
    exact hsecondsum
  8. L51
    exact hpartition_witness_witness_witness_right_left
08Calculate and transport equalitiesL52–52

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

  1. L52
    rewrite heq at hpartition_witness_witness_witness_right_right
09Use earlier factsL53–53

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

  1. L53
    exact hpartition_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 53 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro ab
  6. 0006intro ac
  7. 0007intro bb
  8. 0008intro bc
  9. 0009intro N
  10. 0010intro T
  11. 0011intro hfirst
  12. 0012intro hsecond
  13. 0013intro hfirstsum
  14. 0014intro hsecondsum
  15. 0015have hpartition : ∃ db. ∃ dc. ∃ M. (∀ x. Lt(x,h) → ∃ y. BetaAt(db,dc,x,y) ∧ (∃ z. ∃ n. ∃ m. BetaAt(ab,ac,x,z) ∧ (∃ i. ∃ j. (∀ u. Lt(u,k) → ∃ v. BetaAt(i,j,u,v) ∧ (v = 0 ∧ (Lt(q · S x,p · S u) ∧ ¬Lt(p · S u,q · S x)) ∨ v = 1 ∧ (Lt(p · S u,q · S x) ∧ ¬Lt(q · S x,p · S u)))) ∧ BitCount(i,j,k,z)) ∧ (∀ i. Lt(i,k) → ∃ j. BetaAt(n,m,i,j) ∧ (∃ u. ∃ v. ∃ w. BetaAt(bb,bc,i,u) ∧ (∀ x0. Lt(x0,h) → ∃ x1. BetaAt(v,w,x0,x1) ∧ (x1 = 0 ∧ (Lt(p · S i,q · S x0) ∧ ¬Lt(q · S x0,p · S i)) ∨ x1 = 1 ∧ (Lt(q · S x0,p · S i) ∧ ¬Lt(p · S i,q · S x0)))) ∧ BitCount(v,w,h,u) ∧ BetaAt(v,w,x,j))) ∧ (BitCount(n,m,k,y) ∧ z + y = k))) ∧ (Sum(db,dc,h,M) ∧ N + M = h · k)
    Exact native replay linehave hpartition : exists db dc M. ((forall etcc_row_index_fubini_total_identity_partition_prefix. (exists edt_lt_gap_fubini_total_identity_partition_prefix_bound. edt_lt_gap_fubini_total_identity_partition_prefix_bound + S (etcc_row_index_fubini_total_identity_partition_prefix) = h) -> exists etcc_count_fubini_total_identity_partition_prefix. ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_decoded. ff_h_etcc_fubini_total_identity_partition_prefix_decoded + S (etcc_count_fubini_total_identity_partition_prefix) = S ((S (etcc_row_index_fubini_total_identity_partition_prefix)) * dc)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_decoded. db = ff_q_etcc_fubini_total_identity_partition_prefix_decoded * S ((S (etcc_row_index_fubini_total_identity_partition_prefix)) * dc) + (etcc_count_fubini_total_identity_partition_prefix))) /\ (exists etcc_row_count_fubini_total_identity_partition_prefix_witness etcc_column_code_fubini_total_identity_partition_prefix_witness etcc_column_scale_fubini_total_identity_partition_prefix_witness. ((((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_first_entry. ff_h_etcc_fubini_total_identity_partition_prefix_witness_first_entry + S (etcc_row_count_fubini_total_identity_partition_prefix_witness) = S ((S (etcc_row_index_fubini_total_identity_partition_prefix)) * ac)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_first_entry. ab = ff_q_etcc_fubini_total_identity_partition_prefix_witness_first_entry * S ((S (etcc_row_index_fubini_total_identity_partition_prefix)) * ac) + (etcc_row_count_fubini_total_identity_partition_prefix_witness))) /\ (exists erc_row_code_etcc_fubini_total_identity_partition_prefix_witness_row_semantics erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics. ((forall eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row. (exists eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_bound. eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_bound + S (eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row) = k) -> exists eri_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row. ((((exists ff_h_eri_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_decoded. ff_h_eri_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_decoded + S (eri_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row) = S ((S (eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row)) * erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics)) /\ exists ff_q_eri_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_decoded. erc_row_code_etcc_fubini_total_identity_partition_prefix_witness_row_semantics = ff_q_eri_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_decoded * S ((S (eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row)) * erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics) + (eri_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row))) /\ (((eri_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row = 0 /\ ((exists eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_left + S (q * S etcc_row_index_fubini_total_identity_partition_prefix) = p * S eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row) /\ ~(exists eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row) = q * S etcc_row_index_fubini_total_identity_partition_prefix))) \/ (eri_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row = 1 /\ ((exists eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row) = q * S etcc_row_index_fubini_total_identity_partition_prefix) /\ ~(exists eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_left + S (q * S etcc_row_index_fubini_total_identity_partition_prefix) = p * S eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row))))))) /\ (((exists ff_u_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_start. ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_start. ff_u_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_start * S ((S (0)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) + (0))) /\ ((((exists ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_terminal. ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_terminal + S (etcc_row_count_fubini_total_identity_partition_prefix_witness) = S ((S (k)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_terminal. ff_u_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_terminal * S ((S (k)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) + (etcc_row_count_fubini_total_identity_partition_prefix_witness))) /\ forall ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum. (exists ff_lt_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_bound. ff_lt_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_bound + S ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum = k) -> exists ff_a_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum ff_r_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum ff_s_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_summand. ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_summand + S (ff_a_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) * erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics)) /\ exists ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_summand. erc_row_code_etcc_fubini_total_identity_partition_prefix_witness_row_semantics = ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_summand * S ((S (ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) * erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics) + (ff_a_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_partial. ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_partial + S (ff_r_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_partial. ff_u_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_partial * S ((S (ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) + (ff_r_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_successor. ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_successor + S (ff_s_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) = S ((S (S ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_successor. ff_u_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_successor * S ((S (S ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) + (ff_s_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum))) /\ ff_s_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum = ff_r_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum + ff_a_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)))))) /\ (forall ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits. (exists ff_lt_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits_bound. ff_lt_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits_bound + S ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits = k) -> exists ff_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits. ((((exists ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits_decoded. ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits_decoded + S (ff_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits) = S ((S (ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits)) * erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics)) /\ exists ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits_decoded. erc_row_code_etcc_fubini_total_identity_partition_prefix_witness_row_semantics = ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits_decoded * S ((S (ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits)) * erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics) + (ff_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits))) /\ (ff_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits = 0 \/ ff_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits = 1)))))))) /\ (forall etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column. (exists edt_lt_gap_etcc_fubini_total_identity_partition_prefix_witness_column_bound. edt_lt_gap_etcc_fubini_total_identity_partition_prefix_witness_column_bound + S (etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column) = k) -> exists etc_bit_etcc_fubini_total_identity_partition_prefix_witness_column. ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_decoded. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_decoded + S (etc_bit_etcc_fubini_total_identity_partition_prefix_witness_column) = S ((S (etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column)) * etcc_column_scale_fubini_total_identity_partition_prefix_witness)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_decoded. etcc_column_code_fubini_total_identity_partition_prefix_witness = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_decoded * S ((S (etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column)) * etcc_column_scale_fubini_total_identity_partition_prefix_witness) + (etc_bit_etcc_fubini_total_identity_partition_prefix_witness_column))) /\ (exists etc_count_etcc_fubini_total_identity_partition_prefix_witness_column_witness etc_row_code_etcc_fubini_total_identity_partition_prefix_witness_column_witness etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness. ((((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_outer_entry. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_outer_entry + S (etc_count_etcc_fubini_total_identity_partition_prefix_witness_column_witness) = S ((S (etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column)) * bc)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_outer_entry. bb = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_outer_entry * S ((S (etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column)) * bc) + (etc_count_etcc_fubini_total_identity_partition_prefix_witness_column_witness))) /\ (forall eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row. (exists eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_bound. eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_bound + S (eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row) = h) -> exists eri_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row. ((((exists ff_h_eri_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_decoded. ff_h_eri_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_decoded + S (eri_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row) = S ((S (eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness)) /\ exists ff_q_eri_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_decoded. etc_row_code_etcc_fubini_total_identity_partition_prefix_witness_column_witness = ff_q_eri_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_decoded * S ((S (eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness) + (eri_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row))) /\ (((eri_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_left. eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column) = q * S eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row) /\ ~(exists eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_right. eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row) = p * S etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column))) \/ (eri_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_right. eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row) = p * S etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column) /\ ~(exists eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_left. eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column) = q * S eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_start. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_start. ff_u_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_terminal. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_terminal + S (etc_count_etcc_fubini_total_identity_partition_prefix_witness_column_witness) = S ((S (h)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_terminal. ff_u_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) + (etc_count_etcc_fubini_total_identity_partition_prefix_witness_column_witness))) /\ forall ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum. (exists ff_lt_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_bound. ff_lt_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_bound + S ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum = h) -> exists ff_a_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum ff_r_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum ff_s_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_summand. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_summand. etc_row_code_etcc_fubini_total_identity_partition_prefix_witness_column_witness = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness) + (ff_a_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_partial. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_partial. ff_u_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) + (ff_r_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_successor. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_successor. ff_u_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) + (ff_s_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum))) /\ ff_s_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum = ff_r_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum + ff_a_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits. (exists ff_lt_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits_bound. ff_lt_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits_bound + S ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits = h) -> exists ff_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits_decoded. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits_decoded. etc_row_code_etcc_fubini_total_identity_partition_prefix_witness_column_witness = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness) + (ff_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_inner_entry. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_inner_entry + S (etc_bit_etcc_fubini_total_identity_partition_prefix_witness_column) = S ((S (etcc_row_index_fubini_total_identity_partition_prefix)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_inner_entry. etc_row_code_etcc_fubini_total_identity_partition_prefix_witness_column_witness = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_inner_entry * S ((S (etcc_row_index_fubini_total_identity_partition_prefix)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness) + (etc_bit_etcc_fubini_total_identity_partition_prefix_witness_column)))))))) /\ ((((exists ff_u_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum. ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_start. ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_start + S (0) = S ((S (0)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_start. ff_u_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum = ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_start * S ((S (0)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) + (0))) /\ ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_terminal. ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_terminal + S (etcc_count_fubini_total_identity_partition_prefix) = S ((S (k)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_terminal. ff_u_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum = ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_terminal * S ((S (k)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) + (etcc_count_fubini_total_identity_partition_prefix))) /\ forall ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum. (exists ff_lt_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_bound. ff_lt_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_bound + S ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum = k) -> exists ff_a_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum ff_r_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum ff_s_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum. ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_summand. ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_summand + S (ff_a_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) = S ((S (ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) * etcc_column_scale_fubini_total_identity_partition_prefix_witness)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_summand. etcc_column_code_fubini_total_identity_partition_prefix_witness = ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_summand * S ((S (ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) * etcc_column_scale_fubini_total_identity_partition_prefix_witness) + (ff_a_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum))) /\ ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_partial. ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_partial + S (ff_r_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) = S ((S (ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_partial. ff_u_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum = ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_partial * S ((S (ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) + (ff_r_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum))) /\ ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_successor. ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_successor + S (ff_s_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) = S ((S (S ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_successor. ff_u_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum = ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_successor * S ((S (S ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) + (ff_s_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum))) /\ ff_s_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum = ff_r_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum + ff_a_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)))))) /\ (forall ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits. (exists ff_lt_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits_bound. ff_lt_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits_bound + S ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits = k) -> exists ff_bit_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits. ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits_decoded. ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits_decoded + S (ff_bit_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits) = S ((S (ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits)) * etcc_column_scale_fubini_total_identity_partition_prefix_witness)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits_decoded. etcc_column_code_fubini_total_identity_partition_prefix_witness = ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits_decoded * S ((S (ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits)) * etcc_column_scale_fubini_total_identity_partition_prefix_witness) + (ff_bit_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits))) /\ (ff_bit_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits = 0 \/ ff_bit_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits = 1))))) /\ etcc_row_count_fubini_total_identity_partition_prefix_witness + etcc_count_fubini_total_identity_partition_prefix = k))))) /\ ((exists ff_u_fubini_total_identity_partition_sum ff_v_fubini_total_identity_partition_sum. ((((exists ff_h_fubini_total_identity_partition_sum_start. ff_h_fubini_total_identity_partition_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_identity_partition_sum)) /\ exists ff_q_fubini_total_identity_partition_sum_start. ff_u_fubini_total_identity_partition_sum = ff_q_fubini_total_identity_partition_sum_start * S ((S (0)) * ff_v_fubini_total_identity_partition_sum) + (0))) /\ ((((exists ff_h_fubini_total_identity_partition_sum_terminal. ff_h_fubini_total_identity_partition_sum_terminal + S (M) = S ((S (h)) * ff_v_fubini_total_identity_partition_sum)) /\ exists ff_q_fubini_total_identity_partition_sum_terminal. ff_u_fubini_total_identity_partition_sum = ff_q_fubini_total_identity_partition_sum_terminal * S ((S (h)) * ff_v_fubini_total_identity_partition_sum) + (M))) /\ forall ff_i_fubini_total_identity_partition_sum. (exists ff_lt_fubini_total_identity_partition_sum_bound. ff_lt_fubini_total_identity_partition_sum_bound + S ff_i_fubini_total_identity_partition_sum = h) -> exists ff_a_fubini_total_identity_partition_sum ff_r_fubini_total_identity_partition_sum ff_s_fubini_total_identity_partition_sum. ((((exists ff_h_fubini_total_identity_partition_sum_summand. ff_h_fubini_total_identity_partition_sum_summand + S (ff_a_fubini_total_identity_partition_sum) = S ((S (ff_i_fubini_total_identity_partition_sum)) * dc)) /\ exists ff_q_fubini_total_identity_partition_sum_summand. db = ff_q_fubini_total_identity_partition_sum_summand * S ((S (ff_i_fubini_total_identity_partition_sum)) * dc) + (ff_a_fubini_total_identity_partition_sum))) /\ ((((exists ff_h_fubini_total_identity_partition_sum_partial. ff_h_fubini_total_identity_partition_sum_partial + S (ff_r_fubini_total_identity_partition_sum) = S ((S (ff_i_fubini_total_identity_partition_sum)) * ff_v_fubini_total_identity_partition_sum)) /\ exists ff_q_fubini_total_identity_partition_sum_partial. ff_u_fubini_total_identity_partition_sum = ff_q_fubini_total_identity_partition_sum_partial * S ((S (ff_i_fubini_total_identity_partition_sum)) * ff_v_fubini_total_identity_partition_sum) + (ff_r_fubini_total_identity_partition_sum))) /\ ((((exists ff_h_fubini_total_identity_partition_sum_successor. ff_h_fubini_total_identity_partition_sum_successor + S (ff_s_fubini_total_identity_partition_sum) = S ((S (S ff_i_fubini_total_identity_partition_sum)) * ff_v_fubini_total_identity_partition_sum)) /\ exists ff_q_fubini_total_identity_partition_sum_successor. ff_u_fubini_total_identity_partition_sum = ff_q_fubini_total_identity_partition_sum_successor * S ((S (S ff_i_fubini_total_identity_partition_sum)) * ff_v_fubini_total_identity_partition_sum) + (ff_s_fubini_total_identity_partition_sum))) /\ ff_s_fubini_total_identity_partition_sum = ff_r_fubini_total_identity_partition_sum + ff_a_fubini_total_identity_partition_sum)))))) /\ N + M = h * k))
  16. 0016specialize eisenstein_rectangle_plus_column_count_total p
  17. 0017specialize eisenstein_rectangle_plus_column_count_total q
  18. 0018specialize eisenstein_rectangle_plus_column_count_total h
  19. 0019specialize eisenstein_rectangle_plus_column_count_total k
  20. 0020specialize eisenstein_rectangle_plus_column_count_total ab
  21. 0021specialize eisenstein_rectangle_plus_column_count_total ac
  22. 0022specialize eisenstein_rectangle_plus_column_count_total bb
  23. 0023specialize eisenstein_rectangle_plus_column_count_total bc
  24. 0024specialize eisenstein_rectangle_plus_column_count_total N
  25. 0025apply eisenstein_rectangle_plus_column_count_total
  26. 0026exact hfirst
  27. 0027exact hsecond
  28. 0028exact hfirstsum
  29. 0029cases hpartition
  30. 0030cases hpartition_witness
  31. 0031cases hpartition_witness_witness
  32. 0032cases hpartition_witness_witness_witness
  33. 0033cases hpartition_witness_witness_witness_right
  34. 0034have heq : x2 = T
  35. 0035specialize eisenstein_constructed_column_total_equals_swapped_total p
  36. 0036specialize eisenstein_constructed_column_total_equals_swapped_total q
  37. 0037specialize eisenstein_constructed_column_total_equals_swapped_total h
  38. 0038specialize eisenstein_constructed_column_total_equals_swapped_total k
  39. 0039specialize eisenstein_constructed_column_total_equals_swapped_total ab
  40. 0040specialize eisenstein_constructed_column_total_equals_swapped_total ac
  41. 0041specialize eisenstein_constructed_column_total_equals_swapped_total bb
  42. 0042specialize eisenstein_constructed_column_total_equals_swapped_total bc
  43. 0043specialize eisenstein_constructed_column_total_equals_swapped_total x
  44. 0044specialize eisenstein_constructed_column_total_equals_swapped_total x1
  45. 0045specialize eisenstein_constructed_column_total_equals_swapped_total T
  46. 0046specialize eisenstein_constructed_column_total_equals_swapped_total x2
  47. 0047apply eisenstein_constructed_column_total_equals_swapped_total
  48. 0048exact hsecond
  49. 0049exact hpartition_witness_witness_witness_left
  50. 0050exact hsecondsum
  51. 0051exact hpartition_witness_witness_witness_right_left
  52. 0052rewrite heq at hpartition_witness_witness_witness_right_right
  53. 0053exact hpartition_witness_witness_witness_right_right