PA00F6

eisenstein_transposed_column_counts_extensional

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

Counts of extensionally identical semantic transposed columns are equal across arbitrary provenance codes.

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.

Exact expanded PA statement

forall p q hs ht bs cs bt ct i zs es zt et k n m. (forall etc_row_index_fubini_total_source_column. (exists edt_lt_gap_fubini_total_source_column_bound. edt_lt_gap_fubini_total_source_column_bound + S (etc_row_index_fubini_total_source_column) = k) -> exists etc_bit_fubini_total_source_column. ((((exists ff_h_etc_fubini_total_source_column_decoded. ff_h_etc_fubini_total_source_column_decoded + S (etc_bit_fubini_total_source_column) = S ((S (etc_row_index_fubini_total_source_column)) * es)) /\ exists ff_q_etc_fubini_total_source_column_decoded. zs = ff_q_etc_fubini_total_source_column_decoded * S ((S (etc_row_index_fubini_total_source_column)) * es) + (etc_bit_fubini_total_source_column))) /\ (exists etc_count_fubini_total_source_column_witness etc_row_code_fubini_total_source_column_witness etc_row_scale_fubini_total_source_column_witness. ((((((exists ff_h_etc_fubini_total_source_column_witness_outer_entry. ff_h_etc_fubini_total_source_column_witness_outer_entry + S (etc_count_fubini_total_source_column_witness) = S ((S (etc_row_index_fubini_total_source_column)) * cs)) /\ exists ff_q_etc_fubini_total_source_column_witness_outer_entry. bs = ff_q_etc_fubini_total_source_column_witness_outer_entry * S ((S (etc_row_index_fubini_total_source_column)) * cs) + (etc_count_fubini_total_source_column_witness))) /\ (forall eri_column_etc_fubini_total_source_column_witness_row. (exists eri_gap_etc_fubini_total_source_column_witness_row_bound. eri_gap_etc_fubini_total_source_column_witness_row_bound + S (eri_column_etc_fubini_total_source_column_witness_row) = hs) -> exists eri_bit_etc_fubini_total_source_column_witness_row. ((((exists ff_h_eri_etc_fubini_total_source_column_witness_row_decoded. ff_h_eri_etc_fubini_total_source_column_witness_row_decoded + S (eri_bit_etc_fubini_total_source_column_witness_row) = S ((S (eri_column_etc_fubini_total_source_column_witness_row)) * etc_row_scale_fubini_total_source_column_witness)) /\ exists ff_q_eri_etc_fubini_total_source_column_witness_row_decoded. etc_row_code_fubini_total_source_column_witness = ff_q_eri_etc_fubini_total_source_column_witness_row_decoded * S ((S (eri_column_etc_fubini_total_source_column_witness_row)) * etc_row_scale_fubini_total_source_column_witness) + (eri_bit_etc_fubini_total_source_column_witness_row))) /\ (((eri_bit_etc_fubini_total_source_column_witness_row = 0 /\ ((exists eri_gap_etc_fubini_total_source_column_witness_row_choice_left. eri_gap_etc_fubini_total_source_column_witness_row_choice_left + S (p * S etc_row_index_fubini_total_source_column) = q * S eri_column_etc_fubini_total_source_column_witness_row) /\ ~(exists eri_gap_etc_fubini_total_source_column_witness_row_choice_right. eri_gap_etc_fubini_total_source_column_witness_row_choice_right + S (q * S eri_column_etc_fubini_total_source_column_witness_row) = p * S etc_row_index_fubini_total_source_column))) \/ (eri_bit_etc_fubini_total_source_column_witness_row = 1 /\ ((exists eri_gap_etc_fubini_total_source_column_witness_row_choice_right. eri_gap_etc_fubini_total_source_column_witness_row_choice_right + S (q * S eri_column_etc_fubini_total_source_column_witness_row) = p * S etc_row_index_fubini_total_source_column) /\ ~(exists eri_gap_etc_fubini_total_source_column_witness_row_choice_left. eri_gap_etc_fubini_total_source_column_witness_row_choice_left + S (p * S etc_row_index_fubini_total_source_column) = q * S eri_column_etc_fubini_total_source_column_witness_row)))))))) /\ (((exists ff_u_etc_fubini_total_source_column_witness_count_relation_sum ff_v_etc_fubini_total_source_column_witness_count_relation_sum. ((((exists ff_h_etc_fubini_total_source_column_witness_count_relation_sum_start. ff_h_etc_fubini_total_source_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_fubini_total_source_column_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_total_source_column_witness_count_relation_sum_start. ff_u_etc_fubini_total_source_column_witness_count_relation_sum = ff_q_etc_fubini_total_source_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_fubini_total_source_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_fubini_total_source_column_witness_count_relation_sum_terminal. ff_h_etc_fubini_total_source_column_witness_count_relation_sum_terminal + S (etc_count_fubini_total_source_column_witness) = S ((S (hs)) * ff_v_etc_fubini_total_source_column_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_total_source_column_witness_count_relation_sum_terminal. ff_u_etc_fubini_total_source_column_witness_count_relation_sum = ff_q_etc_fubini_total_source_column_witness_count_relation_sum_terminal * S ((S (hs)) * ff_v_etc_fubini_total_source_column_witness_count_relation_sum) + (etc_count_fubini_total_source_column_witness))) /\ forall ff_i_etc_fubini_total_source_column_witness_count_relation_sum. (exists ff_lt_etc_fubini_total_source_column_witness_count_relation_sum_bound. ff_lt_etc_fubini_total_source_column_witness_count_relation_sum_bound + S ff_i_etc_fubini_total_source_column_witness_count_relation_sum = hs) -> exists ff_a_etc_fubini_total_source_column_witness_count_relation_sum ff_r_etc_fubini_total_source_column_witness_count_relation_sum ff_s_etc_fubini_total_source_column_witness_count_relation_sum. ((((exists ff_h_etc_fubini_total_source_column_witness_count_relation_sum_summand. ff_h_etc_fubini_total_source_column_witness_count_relation_sum_summand + S (ff_a_etc_fubini_total_source_column_witness_count_relation_sum) = S ((S (ff_i_etc_fubini_total_source_column_witness_count_relation_sum)) * etc_row_scale_fubini_total_source_column_witness)) /\ exists ff_q_etc_fubini_total_source_column_witness_count_relation_sum_summand. etc_row_code_fubini_total_source_column_witness = ff_q_etc_fubini_total_source_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_fubini_total_source_column_witness_count_relation_sum)) * etc_row_scale_fubini_total_source_column_witness) + (ff_a_etc_fubini_total_source_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_fubini_total_source_column_witness_count_relation_sum_partial. ff_h_etc_fubini_total_source_column_witness_count_relation_sum_partial + S (ff_r_etc_fubini_total_source_column_witness_count_relation_sum) = S ((S (ff_i_etc_fubini_total_source_column_witness_count_relation_sum)) * ff_v_etc_fubini_total_source_column_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_total_source_column_witness_count_relation_sum_partial. ff_u_etc_fubini_total_source_column_witness_count_relation_sum = ff_q_etc_fubini_total_source_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_fubini_total_source_column_witness_count_relation_sum)) * ff_v_etc_fubini_total_source_column_witness_count_relation_sum) + (ff_r_etc_fubini_total_source_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_fubini_total_source_column_witness_count_relation_sum_successor. ff_h_etc_fubini_total_source_column_witness_count_relation_sum_successor + S (ff_s_etc_fubini_total_source_column_witness_count_relation_sum) = S ((S (S ff_i_etc_fubini_total_source_column_witness_count_relation_sum)) * ff_v_etc_fubini_total_source_column_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_total_source_column_witness_count_relation_sum_successor. ff_u_etc_fubini_total_source_column_witness_count_relation_sum = ff_q_etc_fubini_total_source_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_fubini_total_source_column_witness_count_relation_sum)) * ff_v_etc_fubini_total_source_column_witness_count_relation_sum) + (ff_s_etc_fubini_total_source_column_witness_count_relation_sum))) /\ ff_s_etc_fubini_total_source_column_witness_count_relation_sum = ff_r_etc_fubini_total_source_column_witness_count_relation_sum + ff_a_etc_fubini_total_source_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_fubini_total_source_column_witness_count_relation_bits. (exists ff_lt_etc_fubini_total_source_column_witness_count_relation_bits_bound. ff_lt_etc_fubini_total_source_column_witness_count_relation_bits_bound + S ff_i_etc_fubini_total_source_column_witness_count_relation_bits = hs) -> exists ff_bit_etc_fubini_total_source_column_witness_count_relation_bits. ((((exists ff_h_etc_fubini_total_source_column_witness_count_relation_bits_decoded. ff_h_etc_fubini_total_source_column_witness_count_relation_bits_decoded + S (ff_bit_etc_fubini_total_source_column_witness_count_relation_bits) = S ((S (ff_i_etc_fubini_total_source_column_witness_count_relation_bits)) * etc_row_scale_fubini_total_source_column_witness)) /\ exists ff_q_etc_fubini_total_source_column_witness_count_relation_bits_decoded. etc_row_code_fubini_total_source_column_witness = ff_q_etc_fubini_total_source_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_fubini_total_source_column_witness_count_relation_bits)) * etc_row_scale_fubini_total_source_column_witness) + (ff_bit_etc_fubini_total_source_column_witness_count_relation_bits))) /\ (ff_bit_etc_fubini_total_source_column_witness_count_relation_bits = 0 \/ ff_bit_etc_fubini_total_source_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_fubini_total_source_column_witness_inner_entry. ff_h_etc_fubini_total_source_column_witness_inner_entry + S (etc_bit_fubini_total_source_column) = S ((S (i)) * etc_row_scale_fubini_total_source_column_witness)) /\ exists ff_q_etc_fubini_total_source_column_witness_inner_entry. etc_row_code_fubini_total_source_column_witness = ff_q_etc_fubini_total_source_column_witness_inner_entry * S ((S (i)) * etc_row_scale_fubini_total_source_column_witness) + (etc_bit_fubini_total_source_column))))))) -> (forall etc_row_index_fubini_total_target_column. (exists edt_lt_gap_fubini_total_target_column_bound. edt_lt_gap_fubini_total_target_column_bound + S (etc_row_index_fubini_total_target_column) = k) -> exists etc_bit_fubini_total_target_column. ((((exists ff_h_etc_fubini_total_target_column_decoded. ff_h_etc_fubini_total_target_column_decoded + S (etc_bit_fubini_total_target_column) = S ((S (etc_row_index_fubini_total_target_column)) * et)) /\ exists ff_q_etc_fubini_total_target_column_decoded. zt = ff_q_etc_fubini_total_target_column_decoded * S ((S (etc_row_index_fubini_total_target_column)) * et) + (etc_bit_fubini_total_target_column))) /\ (exists etc_count_fubini_total_target_column_witness etc_row_code_fubini_total_target_column_witness etc_row_scale_fubini_total_target_column_witness. ((((((exists ff_h_etc_fubini_total_target_column_witness_outer_entry. ff_h_etc_fubini_total_target_column_witness_outer_entry + S (etc_count_fubini_total_target_column_witness) = S ((S (etc_row_index_fubini_total_target_column)) * ct)) /\ exists ff_q_etc_fubini_total_target_column_witness_outer_entry. bt = ff_q_etc_fubini_total_target_column_witness_outer_entry * S ((S (etc_row_index_fubini_total_target_column)) * ct) + (etc_count_fubini_total_target_column_witness))) /\ (forall eri_column_etc_fubini_total_target_column_witness_row. (exists eri_gap_etc_fubini_total_target_column_witness_row_bound. eri_gap_etc_fubini_total_target_column_witness_row_bound + S (eri_column_etc_fubini_total_target_column_witness_row) = ht) -> exists eri_bit_etc_fubini_total_target_column_witness_row. ((((exists ff_h_eri_etc_fubini_total_target_column_witness_row_decoded. ff_h_eri_etc_fubini_total_target_column_witness_row_decoded + S (eri_bit_etc_fubini_total_target_column_witness_row) = S ((S (eri_column_etc_fubini_total_target_column_witness_row)) * etc_row_scale_fubini_total_target_column_witness)) /\ exists ff_q_eri_etc_fubini_total_target_column_witness_row_decoded. etc_row_code_fubini_total_target_column_witness = ff_q_eri_etc_fubini_total_target_column_witness_row_decoded * S ((S (eri_column_etc_fubini_total_target_column_witness_row)) * etc_row_scale_fubini_total_target_column_witness) + (eri_bit_etc_fubini_total_target_column_witness_row))) /\ (((eri_bit_etc_fubini_total_target_column_witness_row = 0 /\ ((exists eri_gap_etc_fubini_total_target_column_witness_row_choice_left. eri_gap_etc_fubini_total_target_column_witness_row_choice_left + S (p * S etc_row_index_fubini_total_target_column) = q * S eri_column_etc_fubini_total_target_column_witness_row) /\ ~(exists eri_gap_etc_fubini_total_target_column_witness_row_choice_right. eri_gap_etc_fubini_total_target_column_witness_row_choice_right + S (q * S eri_column_etc_fubini_total_target_column_witness_row) = p * S etc_row_index_fubini_total_target_column))) \/ (eri_bit_etc_fubini_total_target_column_witness_row = 1 /\ ((exists eri_gap_etc_fubini_total_target_column_witness_row_choice_right. eri_gap_etc_fubini_total_target_column_witness_row_choice_right + S (q * S eri_column_etc_fubini_total_target_column_witness_row) = p * S etc_row_index_fubini_total_target_column) /\ ~(exists eri_gap_etc_fubini_total_target_column_witness_row_choice_left. eri_gap_etc_fubini_total_target_column_witness_row_choice_left + S (p * S etc_row_index_fubini_total_target_column) = q * S eri_column_etc_fubini_total_target_column_witness_row)))))))) /\ (((exists ff_u_etc_fubini_total_target_column_witness_count_relation_sum ff_v_etc_fubini_total_target_column_witness_count_relation_sum. ((((exists ff_h_etc_fubini_total_target_column_witness_count_relation_sum_start. ff_h_etc_fubini_total_target_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_fubini_total_target_column_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_total_target_column_witness_count_relation_sum_start. ff_u_etc_fubini_total_target_column_witness_count_relation_sum = ff_q_etc_fubini_total_target_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_fubini_total_target_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_fubini_total_target_column_witness_count_relation_sum_terminal. ff_h_etc_fubini_total_target_column_witness_count_relation_sum_terminal + S (etc_count_fubini_total_target_column_witness) = S ((S (ht)) * ff_v_etc_fubini_total_target_column_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_total_target_column_witness_count_relation_sum_terminal. ff_u_etc_fubini_total_target_column_witness_count_relation_sum = ff_q_etc_fubini_total_target_column_witness_count_relation_sum_terminal * S ((S (ht)) * ff_v_etc_fubini_total_target_column_witness_count_relation_sum) + (etc_count_fubini_total_target_column_witness))) /\ forall ff_i_etc_fubini_total_target_column_witness_count_relation_sum. (exists ff_lt_etc_fubini_total_target_column_witness_count_relation_sum_bound. ff_lt_etc_fubini_total_target_column_witness_count_relation_sum_bound + S ff_i_etc_fubini_total_target_column_witness_count_relation_sum = ht) -> exists ff_a_etc_fubini_total_target_column_witness_count_relation_sum ff_r_etc_fubini_total_target_column_witness_count_relation_sum ff_s_etc_fubini_total_target_column_witness_count_relation_sum. ((((exists ff_h_etc_fubini_total_target_column_witness_count_relation_sum_summand. ff_h_etc_fubini_total_target_column_witness_count_relation_sum_summand + S (ff_a_etc_fubini_total_target_column_witness_count_relation_sum) = S ((S (ff_i_etc_fubini_total_target_column_witness_count_relation_sum)) * etc_row_scale_fubini_total_target_column_witness)) /\ exists ff_q_etc_fubini_total_target_column_witness_count_relation_sum_summand. etc_row_code_fubini_total_target_column_witness = ff_q_etc_fubini_total_target_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_fubini_total_target_column_witness_count_relation_sum)) * etc_row_scale_fubini_total_target_column_witness) + (ff_a_etc_fubini_total_target_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_fubini_total_target_column_witness_count_relation_sum_partial. ff_h_etc_fubini_total_target_column_witness_count_relation_sum_partial + S (ff_r_etc_fubini_total_target_column_witness_count_relation_sum) = S ((S (ff_i_etc_fubini_total_target_column_witness_count_relation_sum)) * ff_v_etc_fubini_total_target_column_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_total_target_column_witness_count_relation_sum_partial. ff_u_etc_fubini_total_target_column_witness_count_relation_sum = ff_q_etc_fubini_total_target_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_fubini_total_target_column_witness_count_relation_sum)) * ff_v_etc_fubini_total_target_column_witness_count_relation_sum) + (ff_r_etc_fubini_total_target_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_fubini_total_target_column_witness_count_relation_sum_successor. ff_h_etc_fubini_total_target_column_witness_count_relation_sum_successor + S (ff_s_etc_fubini_total_target_column_witness_count_relation_sum) = S ((S (S ff_i_etc_fubini_total_target_column_witness_count_relation_sum)) * ff_v_etc_fubini_total_target_column_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_total_target_column_witness_count_relation_sum_successor. ff_u_etc_fubini_total_target_column_witness_count_relation_sum = ff_q_etc_fubini_total_target_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_fubini_total_target_column_witness_count_relation_sum)) * ff_v_etc_fubini_total_target_column_witness_count_relation_sum) + (ff_s_etc_fubini_total_target_column_witness_count_relation_sum))) /\ ff_s_etc_fubini_total_target_column_witness_count_relation_sum = ff_r_etc_fubini_total_target_column_witness_count_relation_sum + ff_a_etc_fubini_total_target_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_fubini_total_target_column_witness_count_relation_bits. (exists ff_lt_etc_fubini_total_target_column_witness_count_relation_bits_bound. ff_lt_etc_fubini_total_target_column_witness_count_relation_bits_bound + S ff_i_etc_fubini_total_target_column_witness_count_relation_bits = ht) -> exists ff_bit_etc_fubini_total_target_column_witness_count_relation_bits. ((((exists ff_h_etc_fubini_total_target_column_witness_count_relation_bits_decoded. ff_h_etc_fubini_total_target_column_witness_count_relation_bits_decoded + S (ff_bit_etc_fubini_total_target_column_witness_count_relation_bits) = S ((S (ff_i_etc_fubini_total_target_column_witness_count_relation_bits)) * etc_row_scale_fubini_total_target_column_witness)) /\ exists ff_q_etc_fubini_total_target_column_witness_count_relation_bits_decoded. etc_row_code_fubini_total_target_column_witness = ff_q_etc_fubini_total_target_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_fubini_total_target_column_witness_count_relation_bits)) * etc_row_scale_fubini_total_target_column_witness) + (ff_bit_etc_fubini_total_target_column_witness_count_relation_bits))) /\ (ff_bit_etc_fubini_total_target_column_witness_count_relation_bits = 0 \/ ff_bit_etc_fubini_total_target_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_fubini_total_target_column_witness_inner_entry. ff_h_etc_fubini_total_target_column_witness_inner_entry + S (etc_bit_fubini_total_target_column) = S ((S (i)) * etc_row_scale_fubini_total_target_column_witness)) /\ exists ff_q_etc_fubini_total_target_column_witness_inner_entry. etc_row_code_fubini_total_target_column_witness = ff_q_etc_fubini_total_target_column_witness_inner_entry * S ((S (i)) * etc_row_scale_fubini_total_target_column_witness) + (etc_bit_fubini_total_target_column))))))) -> (exists edt_lt_gap_fubini_total_source_fixed_bound. edt_lt_gap_fubini_total_source_fixed_bound + S (i) = hs) -> (exists edt_lt_gap_fubini_total_target_fixed_bound. edt_lt_gap_fubini_total_target_fixed_bound + S (i) = ht) -> (((exists ff_u_fubini_total_source_count_sum ff_v_fubini_total_source_count_sum. ((((exists ff_h_fubini_total_source_count_sum_start. ff_h_fubini_total_source_count_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_source_count_sum)) /\ exists ff_q_fubini_total_source_count_sum_start. ff_u_fubini_total_source_count_sum = ff_q_fubini_total_source_count_sum_start * S ((S (0)) * ff_v_fubini_total_source_count_sum) + (0))) /\ ((((exists ff_h_fubini_total_source_count_sum_terminal. ff_h_fubini_total_source_count_sum_terminal + S (n) = S ((S (k)) * ff_v_fubini_total_source_count_sum)) /\ exists ff_q_fubini_total_source_count_sum_terminal. ff_u_fubini_total_source_count_sum = ff_q_fubini_total_source_count_sum_terminal * S ((S (k)) * ff_v_fubini_total_source_count_sum) + (n))) /\ forall ff_i_fubini_total_source_count_sum. (exists ff_lt_fubini_total_source_count_sum_bound. ff_lt_fubini_total_source_count_sum_bound + S ff_i_fubini_total_source_count_sum = k) -> exists ff_a_fubini_total_source_count_sum ff_r_fubini_total_source_count_sum ff_s_fubini_total_source_count_sum. ((((exists ff_h_fubini_total_source_count_sum_summand. ff_h_fubini_total_source_count_sum_summand + S (ff_a_fubini_total_source_count_sum) = S ((S (ff_i_fubini_total_source_count_sum)) * es)) /\ exists ff_q_fubini_total_source_count_sum_summand. zs = ff_q_fubini_total_source_count_sum_summand * S ((S (ff_i_fubini_total_source_count_sum)) * es) + (ff_a_fubini_total_source_count_sum))) /\ ((((exists ff_h_fubini_total_source_count_sum_partial. ff_h_fubini_total_source_count_sum_partial + S (ff_r_fubini_total_source_count_sum) = S ((S (ff_i_fubini_total_source_count_sum)) * ff_v_fubini_total_source_count_sum)) /\ exists ff_q_fubini_total_source_count_sum_partial. ff_u_fubini_total_source_count_sum = ff_q_fubini_total_source_count_sum_partial * S ((S (ff_i_fubini_total_source_count_sum)) * ff_v_fubini_total_source_count_sum) + (ff_r_fubini_total_source_count_sum))) /\ ((((exists ff_h_fubini_total_source_count_sum_successor. ff_h_fubini_total_source_count_sum_successor + S (ff_s_fubini_total_source_count_sum) = S ((S (S ff_i_fubini_total_source_count_sum)) * ff_v_fubini_total_source_count_sum)) /\ exists ff_q_fubini_total_source_count_sum_successor. ff_u_fubini_total_source_count_sum = ff_q_fubini_total_source_count_sum_successor * S ((S (S ff_i_fubini_total_source_count_sum)) * ff_v_fubini_total_source_count_sum) + (ff_s_fubini_total_source_count_sum))) /\ ff_s_fubini_total_source_count_sum = ff_r_fubini_total_source_count_sum + ff_a_fubini_total_source_count_sum)))))) /\ (forall ff_i_fubini_total_source_count_bits. (exists ff_lt_fubini_total_source_count_bits_bound. ff_lt_fubini_total_source_count_bits_bound + S ff_i_fubini_total_source_count_bits = k) -> exists ff_bit_fubini_total_source_count_bits. ((((exists ff_h_fubini_total_source_count_bits_decoded. ff_h_fubini_total_source_count_bits_decoded + S (ff_bit_fubini_total_source_count_bits) = S ((S (ff_i_fubini_total_source_count_bits)) * es)) /\ exists ff_q_fubini_total_source_count_bits_decoded. zs = ff_q_fubini_total_source_count_bits_decoded * S ((S (ff_i_fubini_total_source_count_bits)) * es) + (ff_bit_fubini_total_source_count_bits))) /\ (ff_bit_fubini_total_source_count_bits = 0 \/ ff_bit_fubini_total_source_count_bits = 1))))) -> (((exists ff_u_fubini_total_target_count_sum ff_v_fubini_total_target_count_sum. ((((exists ff_h_fubini_total_target_count_sum_start. ff_h_fubini_total_target_count_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_target_count_sum)) /\ exists ff_q_fubini_total_target_count_sum_start. ff_u_fubini_total_target_count_sum = ff_q_fubini_total_target_count_sum_start * S ((S (0)) * ff_v_fubini_total_target_count_sum) + (0))) /\ ((((exists ff_h_fubini_total_target_count_sum_terminal. ff_h_fubini_total_target_count_sum_terminal + S (m) = S ((S (k)) * ff_v_fubini_total_target_count_sum)) /\ exists ff_q_fubini_total_target_count_sum_terminal. ff_u_fubini_total_target_count_sum = ff_q_fubini_total_target_count_sum_terminal * S ((S (k)) * ff_v_fubini_total_target_count_sum) + (m))) /\ forall ff_i_fubini_total_target_count_sum. (exists ff_lt_fubini_total_target_count_sum_bound. ff_lt_fubini_total_target_count_sum_bound + S ff_i_fubini_total_target_count_sum = k) -> exists ff_a_fubini_total_target_count_sum ff_r_fubini_total_target_count_sum ff_s_fubini_total_target_count_sum. ((((exists ff_h_fubini_total_target_count_sum_summand. ff_h_fubini_total_target_count_sum_summand + S (ff_a_fubini_total_target_count_sum) = S ((S (ff_i_fubini_total_target_count_sum)) * et)) /\ exists ff_q_fubini_total_target_count_sum_summand. zt = ff_q_fubini_total_target_count_sum_summand * S ((S (ff_i_fubini_total_target_count_sum)) * et) + (ff_a_fubini_total_target_count_sum))) /\ ((((exists ff_h_fubini_total_target_count_sum_partial. ff_h_fubini_total_target_count_sum_partial + S (ff_r_fubini_total_target_count_sum) = S ((S (ff_i_fubini_total_target_count_sum)) * ff_v_fubini_total_target_count_sum)) /\ exists ff_q_fubini_total_target_count_sum_partial. ff_u_fubini_total_target_count_sum = ff_q_fubini_total_target_count_sum_partial * S ((S (ff_i_fubini_total_target_count_sum)) * ff_v_fubini_total_target_count_sum) + (ff_r_fubini_total_target_count_sum))) /\ ((((exists ff_h_fubini_total_target_count_sum_successor. ff_h_fubini_total_target_count_sum_successor + S (ff_s_fubini_total_target_count_sum) = S ((S (S ff_i_fubini_total_target_count_sum)) * ff_v_fubini_total_target_count_sum)) /\ exists ff_q_fubini_total_target_count_sum_successor. ff_u_fubini_total_target_count_sum = ff_q_fubini_total_target_count_sum_successor * S ((S (S ff_i_fubini_total_target_count_sum)) * ff_v_fubini_total_target_count_sum) + (ff_s_fubini_total_target_count_sum))) /\ ff_s_fubini_total_target_count_sum = ff_r_fubini_total_target_count_sum + ff_a_fubini_total_target_count_sum)))))) /\ (forall ff_i_fubini_total_target_count_bits. (exists ff_lt_fubini_total_target_count_bits_bound. ff_lt_fubini_total_target_count_bits_bound + S ff_i_fubini_total_target_count_bits = k) -> exists ff_bit_fubini_total_target_count_bits. ((((exists ff_h_fubini_total_target_count_bits_decoded. ff_h_fubini_total_target_count_bits_decoded + S (ff_bit_fubini_total_target_count_bits) = S ((S (ff_i_fubini_total_target_count_bits)) * et)) /\ exists ff_q_fubini_total_target_count_bits_decoded. zt = ff_q_fubini_total_target_count_bits_decoded * S ((S (ff_i_fubini_total_target_count_bits)) * et) + (ff_bit_fubini_total_target_count_bits))) /\ (ff_bit_fubini_total_target_count_bits = 0 \/ ff_bit_fubini_total_target_count_bits = 1))))) -> n = m

Structural proof guide

Generated structural guide

Counts of extensionally identical semantic transposed columns are equal across arbitrary provenance codes.

Use the direct prerequisites beta_at_exists, eisenstein_transposed_column_decoded_choice, eisenstein_cell_indicator_choice_unique, beta_sum_transport_prefix, beta_sum_functional as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (6), equality transport (2).

Referenced ingredients

PA0029 beta_at_exists PA00F4 eisenstein_transposed_column_decoded_choice PA00F5 eisenstein_cell_indicator_choice_unique PA00CT beta_sum_transport_prefix PA006P beta_sum_functional

Proof neighborhood

Direct dependencies

PA0029 beta_at_exists PA00F4 eisenstein_transposed_column_decoded_choice PA00F5 eisenstein_cell_indicator_choice_unique PA00CT beta_sum_transport_prefix PA006P beta_sum_functional

Direct dependents

PA00F7 eisenstein_fubini_column_count_witness_retarget

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

100 script commands · 16 reading checkpoints · 6 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.

Named ingredients (5)
beta at existseisenstein transposed column decoded choiceeisenstein cell indicator choice uniquebeta sum transport prefixbeta sum functional

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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 hs
  4. L4
    intro ht
  5. L5
    intro bs
  6. L6
    intro cs
  7. L7
    intro bt
  8. L8
    intro ct
  9. L9
    intro i
  10. L10
    intro zs
02Fix variables and assumptionsL11–20

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

  1. L11
    intro es
  2. L12
    intro zt
  3. L13
    intro et
  4. L14
    intro k
  5. L15
    intro n
  6. L16
    intro m
  7. L17
    intro hsource
  8. L18
    intro htarget
  9. L19
    intro his
  10. L20
    intro hit
03Fix variables and assumptionsL21–22

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

  1. L21
    intro hn
  2. L22
    intro hm
04Separate the logical casesL23–24

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

  1. L23
    cases hn
  2. L24
    cases hm
05Establish htransportL25–29

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

  1. L25
    have htransport : ∀ j. ∀ a. Lt(j,k) → BetaAt(zs,es,j,a) → BetaAt(zt,et,j,a)Definitions: LtBetaAt
  2. L26
    intro j
  3. L27
    intro a
  4. L28
    intro hj
  5. L29
    intro ha
06Establish htarget_entryL30–34

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

  1. L30
    have htarget_entry : exists d. (((exists ff_h_fubini_total_extensional_target_entry. ff_h_fubini_total_extensional_target_entry + S (d) = S ((S (j)) * et)) /\ exists ff_q_fubini_total_extensional_target_entry. zt = ff_q_fubini_total_extensional_target_entry * S ((S (j)) * et) + (d)))
  2. L31
    specialize beta_at_exists zt
  3. L32
    specialize beta_at_exists et
  4. L33
    specialize beta_at_exists j
  5. L34
    exact beta_at_exists
07Separate the logical casesL35–35

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

  1. L35
    cases htarget_entry
08Establish hsource_choiceL36–45

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

  1. L36
    have hsource_choice : a = 0 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)) ∨ a = 1 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i))Definitions: Lt
  2. L37
    specialize eisenstein_transposed_column_decoded_choice p
  3. L38
    specialize eisenstein_transposed_column_decoded_choice q
  4. L39
    specialize eisenstein_transposed_column_decoded_choice hs
  5. L40
    specialize eisenstein_transposed_column_decoded_choice bs
  6. L41
    specialize eisenstein_transposed_column_decoded_choice cs
  7. L42
    specialize eisenstein_transposed_column_decoded_choice i
  8. L43
    specialize eisenstein_transposed_column_decoded_choice zs
  9. L44
    specialize eisenstein_transposed_column_decoded_choice es
  10. L45
    specialize eisenstein_transposed_column_decoded_choice k
09Use earlier factsL46–52

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

  1. L46
    specialize eisenstein_transposed_column_decoded_choice j
  2. L47
    specialize eisenstein_transposed_column_decoded_choice a
  3. L48
    apply eisenstein_transposed_column_decoded_choice
  4. L49
    exact hsource
  5. L50
    exact his
  6. L51
    exact hj
  7. L52
    exact ha
10Establish htarget_choiceL53–62

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

  1. L53
    have htarget_choice : x = 0 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)) ∨ x = 1 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i))Definitions: Lt
  2. L54
    specialize eisenstein_transposed_column_decoded_choice p
  3. L55
    specialize eisenstein_transposed_column_decoded_choice q
  4. L56
    specialize eisenstein_transposed_column_decoded_choice ht
  5. L57
    specialize eisenstein_transposed_column_decoded_choice bt
  6. L58
    specialize eisenstein_transposed_column_decoded_choice ct
  7. L59
    specialize eisenstein_transposed_column_decoded_choice i
  8. L60
    specialize eisenstein_transposed_column_decoded_choice zt
  9. L61
    specialize eisenstein_transposed_column_decoded_choice et
  10. L62
    specialize eisenstein_transposed_column_decoded_choice k
11Use earlier factsL63–69

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

  1. L63
    specialize eisenstein_transposed_column_decoded_choice j
  2. L64
    specialize eisenstein_transposed_column_decoded_choice x
  3. L65
    apply eisenstein_transposed_column_decoded_choice
  4. L66
    exact htarget
  5. L67
    exact hit
  6. L68
    exact hj
  7. L69
    exact htarget_entry_witness
12Establish haxL70–79

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

  1. L70
    have hax : a = x
  2. L71
    specialize eisenstein_cell_indicator_choice_unique q
  3. L72
    specialize eisenstein_cell_indicator_choice_unique p
  4. L73
    specialize eisenstein_cell_indicator_choice_unique j
  5. L74
    specialize eisenstein_cell_indicator_choice_unique i
  6. L75
    specialize eisenstein_cell_indicator_choice_unique a
  7. L76
    specialize eisenstein_cell_indicator_choice_unique x
  8. L77
    apply eisenstein_cell_indicator_choice_unique
  9. L78
    exact hsource_choice
  10. L79
    exact htarget_choice
13Calculate and transport equalitiesL80–81

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

  1. L80
    rewrite <- hax at htarget_entry_witness
  2. L81
    rewrite <- hax at htarget_entry_witness
14Use earlier factsL82–82

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

  1. L82
    exact htarget_entry_witness
15Establish htarget_nL83–92

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

  1. L83
    have htarget_n : Sum(zt,et,k,n)Definitions: Sum
  2. L84
    specialize beta_sum_transport_prefix zs
  3. L85
    specialize beta_sum_transport_prefix es
  4. L86
    specialize beta_sum_transport_prefix zt
  5. L87
    specialize beta_sum_transport_prefix et
  6. L88
    specialize beta_sum_transport_prefix k
  7. L89
    specialize beta_sum_transport_prefix n
  8. L90
    apply beta_sum_transport_prefix
  9. L91
    exact hn_left
  10. L92
    exact htransport
16Use earlier factsL93–100

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

  1. L93
    specialize beta_sum_functional zt
  2. L94
    specialize beta_sum_functional et
  3. L95
    specialize beta_sum_functional k
  4. L96
    specialize beta_sum_functional n
  5. L97
    specialize beta_sum_functional m
  6. L98
    apply beta_sum_functional
  7. L99
    exact htarget_n
  8. L100
    exact hm_left

Library-wide reading audit

Original exact command ledger · 100 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro hs
  4. 0004intro ht
  5. 0005intro bs
  6. 0006intro cs
  7. 0007intro bt
  8. 0008intro ct
  9. 0009intro i
  10. 0010intro zs
  11. 0011intro es
  12. 0012intro zt
  13. 0013intro et
  14. 0014intro k
  15. 0015intro n
  16. 0016intro m
  17. 0017intro hsource
  18. 0018intro htarget
  19. 0019intro his
  20. 0020intro hit
  21. 0021intro hn
  22. 0022intro hm
  23. 0023cases hn
  24. 0024cases hm
  25. 0025have htransport : forall j a. (exists edt_lt_gap_fubini_total_extensional_transport_bound. edt_lt_gap_fubini_total_extensional_transport_bound + S (j) = k) -> (((exists ff_h_fubini_total_extensional_transport_source. ff_h_fubini_total_extensional_transport_source + S (a) = S ((S (j)) * es)) /\ exists ff_q_fubini_total_extensional_transport_source. zs = ff_q_fubini_total_extensional_transport_source * S ((S (j)) * es) + (a))) -> (((exists ff_h_fubini_total_extensional_transport_target. ff_h_fubini_total_extensional_transport_target + S (a) = S ((S (j)) * et)) /\ exists ff_q_fubini_total_extensional_transport_target. zt = ff_q_fubini_total_extensional_transport_target * S ((S (j)) * et) + (a)))
  26. 0026intro j
  27. 0027intro a
  28. 0028intro hj
  29. 0029intro ha
  30. 0030have htarget_entry : exists d. (((exists ff_h_fubini_total_extensional_target_entry. ff_h_fubini_total_extensional_target_entry + S (d) = S ((S (j)) * et)) /\ exists ff_q_fubini_total_extensional_target_entry. zt = ff_q_fubini_total_extensional_target_entry * S ((S (j)) * et) + (d)))
  31. 0031specialize beta_at_exists zt
  32. 0032specialize beta_at_exists et
  33. 0033specialize beta_at_exists j
  34. 0034exact beta_at_exists
  35. 0035cases htarget_entry
  36. 0036have hsource_choice : ((a = 0 /\ ((exists eri_gap_fubini_total_extensional_source_choice_left. eri_gap_fubini_total_extensional_source_choice_left + S (p * S j) = q * S i) /\ ~(exists eri_gap_fubini_total_extensional_source_choice_right. eri_gap_fubini_total_extensional_source_choice_right + S (q * S i) = p * S j))) \/ (a = 1 /\ ((exists eri_gap_fubini_total_extensional_source_choice_right. eri_gap_fubini_total_extensional_source_choice_right + S (q * S i) = p * S j) /\ ~(exists eri_gap_fubini_total_extensional_source_choice_left. eri_gap_fubini_total_extensional_source_choice_left + S (p * S j) = q * S i))))
  37. 0037specialize eisenstein_transposed_column_decoded_choice p
  38. 0038specialize eisenstein_transposed_column_decoded_choice q
  39. 0039specialize eisenstein_transposed_column_decoded_choice hs
  40. 0040specialize eisenstein_transposed_column_decoded_choice bs
  41. 0041specialize eisenstein_transposed_column_decoded_choice cs
  42. 0042specialize eisenstein_transposed_column_decoded_choice i
  43. 0043specialize eisenstein_transposed_column_decoded_choice zs
  44. 0044specialize eisenstein_transposed_column_decoded_choice es
  45. 0045specialize eisenstein_transposed_column_decoded_choice k
  46. 0046specialize eisenstein_transposed_column_decoded_choice j
  47. 0047specialize eisenstein_transposed_column_decoded_choice a
  48. 0048apply eisenstein_transposed_column_decoded_choice
  49. 0049exact hsource
  50. 0050exact his
  51. 0051exact hj
  52. 0052exact ha
  53. 0053have htarget_choice : ((x = 0 /\ ((exists eri_gap_fubini_total_extensional_target_choice_left. eri_gap_fubini_total_extensional_target_choice_left + S (p * S j) = q * S i) /\ ~(exists eri_gap_fubini_total_extensional_target_choice_right. eri_gap_fubini_total_extensional_target_choice_right + S (q * S i) = p * S j))) \/ (x = 1 /\ ((exists eri_gap_fubini_total_extensional_target_choice_right. eri_gap_fubini_total_extensional_target_choice_right + S (q * S i) = p * S j) /\ ~(exists eri_gap_fubini_total_extensional_target_choice_left. eri_gap_fubini_total_extensional_target_choice_left + S (p * S j) = q * S i))))
  54. 0054specialize eisenstein_transposed_column_decoded_choice p
  55. 0055specialize eisenstein_transposed_column_decoded_choice q
  56. 0056specialize eisenstein_transposed_column_decoded_choice ht
  57. 0057specialize eisenstein_transposed_column_decoded_choice bt
  58. 0058specialize eisenstein_transposed_column_decoded_choice ct
  59. 0059specialize eisenstein_transposed_column_decoded_choice i
  60. 0060specialize eisenstein_transposed_column_decoded_choice zt
  61. 0061specialize eisenstein_transposed_column_decoded_choice et
  62. 0062specialize eisenstein_transposed_column_decoded_choice k
  63. 0063specialize eisenstein_transposed_column_decoded_choice j
  64. 0064specialize eisenstein_transposed_column_decoded_choice x
  65. 0065apply eisenstein_transposed_column_decoded_choice
  66. 0066exact htarget
  67. 0067exact hit
  68. 0068exact hj
  69. 0069exact htarget_entry_witness
  70. 0070have hax : a = x
  71. 0071specialize eisenstein_cell_indicator_choice_unique q
  72. 0072specialize eisenstein_cell_indicator_choice_unique p
  73. 0073specialize eisenstein_cell_indicator_choice_unique j
  74. 0074specialize eisenstein_cell_indicator_choice_unique i
  75. 0075specialize eisenstein_cell_indicator_choice_unique a
  76. 0076specialize eisenstein_cell_indicator_choice_unique x
  77. 0077apply eisenstein_cell_indicator_choice_unique
  78. 0078exact hsource_choice
  79. 0079exact htarget_choice
  80. 0080rewrite <- hax at htarget_entry_witness
  81. 0081rewrite <- hax at htarget_entry_witness
  82. 0082exact htarget_entry_witness
  83. 0083have htarget_n : exists ff_u_fubini_total_extensional_transported_sum ff_v_fubini_total_extensional_transported_sum. ((((exists ff_h_fubini_total_extensional_transported_sum_start. ff_h_fubini_total_extensional_transported_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_extensional_transported_sum)) /\ exists ff_q_fubini_total_extensional_transported_sum_start. ff_u_fubini_total_extensional_transported_sum = ff_q_fubini_total_extensional_transported_sum_start * S ((S (0)) * ff_v_fubini_total_extensional_transported_sum) + (0))) /\ ((((exists ff_h_fubini_total_extensional_transported_sum_terminal. ff_h_fubini_total_extensional_transported_sum_terminal + S (n) = S ((S (k)) * ff_v_fubini_total_extensional_transported_sum)) /\ exists ff_q_fubini_total_extensional_transported_sum_terminal. ff_u_fubini_total_extensional_transported_sum = ff_q_fubini_total_extensional_transported_sum_terminal * S ((S (k)) * ff_v_fubini_total_extensional_transported_sum) + (n))) /\ forall ff_i_fubini_total_extensional_transported_sum. (exists ff_lt_fubini_total_extensional_transported_sum_bound. ff_lt_fubini_total_extensional_transported_sum_bound + S ff_i_fubini_total_extensional_transported_sum = k) -> exists ff_a_fubini_total_extensional_transported_sum ff_r_fubini_total_extensional_transported_sum ff_s_fubini_total_extensional_transported_sum. ((((exists ff_h_fubini_total_extensional_transported_sum_summand. ff_h_fubini_total_extensional_transported_sum_summand + S (ff_a_fubini_total_extensional_transported_sum) = S ((S (ff_i_fubini_total_extensional_transported_sum)) * et)) /\ exists ff_q_fubini_total_extensional_transported_sum_summand. zt = ff_q_fubini_total_extensional_transported_sum_summand * S ((S (ff_i_fubini_total_extensional_transported_sum)) * et) + (ff_a_fubini_total_extensional_transported_sum))) /\ ((((exists ff_h_fubini_total_extensional_transported_sum_partial. ff_h_fubini_total_extensional_transported_sum_partial + S (ff_r_fubini_total_extensional_transported_sum) = S ((S (ff_i_fubini_total_extensional_transported_sum)) * ff_v_fubini_total_extensional_transported_sum)) /\ exists ff_q_fubini_total_extensional_transported_sum_partial. ff_u_fubini_total_extensional_transported_sum = ff_q_fubini_total_extensional_transported_sum_partial * S ((S (ff_i_fubini_total_extensional_transported_sum)) * ff_v_fubini_total_extensional_transported_sum) + (ff_r_fubini_total_extensional_transported_sum))) /\ ((((exists ff_h_fubini_total_extensional_transported_sum_successor. ff_h_fubini_total_extensional_transported_sum_successor + S (ff_s_fubini_total_extensional_transported_sum) = S ((S (S ff_i_fubini_total_extensional_transported_sum)) * ff_v_fubini_total_extensional_transported_sum)) /\ exists ff_q_fubini_total_extensional_transported_sum_successor. ff_u_fubini_total_extensional_transported_sum = ff_q_fubini_total_extensional_transported_sum_successor * S ((S (S ff_i_fubini_total_extensional_transported_sum)) * ff_v_fubini_total_extensional_transported_sum) + (ff_s_fubini_total_extensional_transported_sum))) /\ ff_s_fubini_total_extensional_transported_sum = ff_r_fubini_total_extensional_transported_sum + ff_a_fubini_total_extensional_transported_sum)))))
  84. 0084specialize beta_sum_transport_prefix zs
  85. 0085specialize beta_sum_transport_prefix es
  86. 0086specialize beta_sum_transport_prefix zt
  87. 0087specialize beta_sum_transport_prefix et
  88. 0088specialize beta_sum_transport_prefix k
  89. 0089specialize beta_sum_transport_prefix n
  90. 0090apply beta_sum_transport_prefix
  91. 0091exact hn_left
  92. 0092exact htransport
  93. 0093specialize beta_sum_functional zt
  94. 0094specialize beta_sum_functional et
  95. 0095specialize beta_sum_functional k
  96. 0096specialize beta_sum_functional n
  97. 0097specialize beta_sum_functional m
  98. 0098apply beta_sum_functional
  99. 0099exact htarget_n
  100. 0100exact hm_left