PA00EN

eisenstein_transposed_column_count_decoded_partition

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

Decoded original-row and constructed-column counts partition the row width.

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 h k ab ac bb bc db dc i n m. (forall etcc_row_index_column_count_semantic_prefix. (exists edt_lt_gap_column_count_semantic_prefix_bound. edt_lt_gap_column_count_semantic_prefix_bound + S (etcc_row_index_column_count_semantic_prefix) = h) -> exists etcc_count_column_count_semantic_prefix. ((((exists ff_h_etcc_column_count_semantic_prefix_decoded. ff_h_etcc_column_count_semantic_prefix_decoded + S (etcc_count_column_count_semantic_prefix) = S ((S (etcc_row_index_column_count_semantic_prefix)) * dc)) /\ exists ff_q_etcc_column_count_semantic_prefix_decoded. db = ff_q_etcc_column_count_semantic_prefix_decoded * S ((S (etcc_row_index_column_count_semantic_prefix)) * dc) + (etcc_count_column_count_semantic_prefix))) /\ (exists etcc_row_count_column_count_semantic_prefix_witness etcc_column_code_column_count_semantic_prefix_witness etcc_column_scale_column_count_semantic_prefix_witness. ((((((exists ff_h_etcc_column_count_semantic_prefix_witness_first_entry. ff_h_etcc_column_count_semantic_prefix_witness_first_entry + S (etcc_row_count_column_count_semantic_prefix_witness) = S ((S (etcc_row_index_column_count_semantic_prefix)) * ac)) /\ exists ff_q_etcc_column_count_semantic_prefix_witness_first_entry. ab = ff_q_etcc_column_count_semantic_prefix_witness_first_entry * S ((S (etcc_row_index_column_count_semantic_prefix)) * ac) + (etcc_row_count_column_count_semantic_prefix_witness))) /\ (exists erc_row_code_etcc_column_count_semantic_prefix_witness_row_semantics erc_row_scale_etcc_column_count_semantic_prefix_witness_row_semantics. ((forall eri_column_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row. (exists eri_gap_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_bound. eri_gap_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_bound + S (eri_column_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row) = k) -> exists eri_bit_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row. ((((exists ff_h_eri_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_decoded. ff_h_eri_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_decoded + S (eri_bit_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row) = S ((S (eri_column_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row)) * erc_row_scale_etcc_column_count_semantic_prefix_witness_row_semantics)) /\ exists ff_q_eri_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_decoded. erc_row_code_etcc_column_count_semantic_prefix_witness_row_semantics = ff_q_eri_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_decoded * S ((S (eri_column_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row)) * erc_row_scale_etcc_column_count_semantic_prefix_witness_row_semantics) + (eri_bit_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row))) /\ (((eri_bit_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row = 0 /\ ((exists eri_gap_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_choice_left + S (q * S etcc_row_index_column_count_semantic_prefix) = p * S eri_column_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row) /\ ~(exists eri_gap_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row) = q * S etcc_row_index_column_count_semantic_prefix))) \/ (eri_bit_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row = 1 /\ ((exists eri_gap_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row) = q * S etcc_row_index_column_count_semantic_prefix) /\ ~(exists eri_gap_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row_choice_left + S (q * S etcc_row_index_column_count_semantic_prefix) = p * S eri_column_erc_etcc_column_count_semantic_prefix_witness_row_semantics_row))))))) /\ (((exists ff_u_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum ff_v_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_start. ff_h_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_start. ff_u_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_start * S ((S (0)) * ff_v_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum) + (0))) /\ ((((exists ff_h_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_terminal. ff_h_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_terminal + S (etcc_row_count_column_count_semantic_prefix_witness) = S ((S (k)) * ff_v_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_terminal. ff_u_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_terminal * S ((S (k)) * ff_v_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum) + (etcc_row_count_column_count_semantic_prefix_witness))) /\ forall ff_i_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum. (exists ff_lt_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_bound. ff_lt_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_bound + S ff_i_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum = k) -> exists ff_a_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum ff_r_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum ff_s_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_summand. ff_h_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_summand + S (ff_a_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum)) * erc_row_scale_etcc_column_count_semantic_prefix_witness_row_semantics)) /\ exists ff_q_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_summand. erc_row_code_etcc_column_count_semantic_prefix_witness_row_semantics = ff_q_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_summand * S ((S (ff_i_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum)) * erc_row_scale_etcc_column_count_semantic_prefix_witness_row_semantics) + (ff_a_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_partial. ff_h_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_partial + S (ff_r_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_partial. ff_u_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_partial * S ((S (ff_i_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum) + (ff_r_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_successor. ff_h_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_successor + S (ff_s_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum) = S ((S (S ff_i_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_successor. ff_u_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum_successor * S ((S (S ff_i_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum) + (ff_s_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum))) /\ ff_s_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum = ff_r_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum + ff_a_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_sum)))))) /\ (forall ff_i_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits. (exists ff_lt_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits_bound. ff_lt_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits_bound + S ff_i_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits = k) -> exists ff_bit_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits. ((((exists ff_h_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits_decoded. ff_h_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits_decoded + S (ff_bit_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits) = S ((S (ff_i_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits)) * erc_row_scale_etcc_column_count_semantic_prefix_witness_row_semantics)) /\ exists ff_q_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits_decoded. erc_row_code_etcc_column_count_semantic_prefix_witness_row_semantics = ff_q_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits_decoded * S ((S (ff_i_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits)) * erc_row_scale_etcc_column_count_semantic_prefix_witness_row_semantics) + (ff_bit_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits))) /\ (ff_bit_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits = 0 \/ ff_bit_erc_etcc_column_count_semantic_prefix_witness_row_semantics_count_bits = 1)))))))) /\ (forall etc_row_index_etcc_column_count_semantic_prefix_witness_column. (exists edt_lt_gap_etcc_column_count_semantic_prefix_witness_column_bound. edt_lt_gap_etcc_column_count_semantic_prefix_witness_column_bound + S (etc_row_index_etcc_column_count_semantic_prefix_witness_column) = k) -> exists etc_bit_etcc_column_count_semantic_prefix_witness_column. ((((exists ff_h_etc_etcc_column_count_semantic_prefix_witness_column_decoded. ff_h_etc_etcc_column_count_semantic_prefix_witness_column_decoded + S (etc_bit_etcc_column_count_semantic_prefix_witness_column) = S ((S (etc_row_index_etcc_column_count_semantic_prefix_witness_column)) * etcc_column_scale_column_count_semantic_prefix_witness)) /\ exists ff_q_etc_etcc_column_count_semantic_prefix_witness_column_decoded. etcc_column_code_column_count_semantic_prefix_witness = ff_q_etc_etcc_column_count_semantic_prefix_witness_column_decoded * S ((S (etc_row_index_etcc_column_count_semantic_prefix_witness_column)) * etcc_column_scale_column_count_semantic_prefix_witness) + (etc_bit_etcc_column_count_semantic_prefix_witness_column))) /\ (exists etc_count_etcc_column_count_semantic_prefix_witness_column_witness etc_row_code_etcc_column_count_semantic_prefix_witness_column_witness etc_row_scale_etcc_column_count_semantic_prefix_witness_column_witness. ((((((exists ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_outer_entry. ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_outer_entry + S (etc_count_etcc_column_count_semantic_prefix_witness_column_witness) = S ((S (etc_row_index_etcc_column_count_semantic_prefix_witness_column)) * bc)) /\ exists ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_outer_entry. bb = ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_outer_entry * S ((S (etc_row_index_etcc_column_count_semantic_prefix_witness_column)) * bc) + (etc_count_etcc_column_count_semantic_prefix_witness_column_witness))) /\ (forall eri_column_etc_etcc_column_count_semantic_prefix_witness_column_witness_row. (exists eri_gap_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_bound. eri_gap_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_bound + S (eri_column_etc_etcc_column_count_semantic_prefix_witness_column_witness_row) = h) -> exists eri_bit_etc_etcc_column_count_semantic_prefix_witness_column_witness_row. ((((exists ff_h_eri_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_decoded. ff_h_eri_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_decoded + S (eri_bit_etc_etcc_column_count_semantic_prefix_witness_column_witness_row) = S ((S (eri_column_etc_etcc_column_count_semantic_prefix_witness_column_witness_row)) * etc_row_scale_etcc_column_count_semantic_prefix_witness_column_witness)) /\ exists ff_q_eri_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_decoded. etc_row_code_etcc_column_count_semantic_prefix_witness_column_witness = ff_q_eri_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_decoded * S ((S (eri_column_etc_etcc_column_count_semantic_prefix_witness_column_witness_row)) * etc_row_scale_etcc_column_count_semantic_prefix_witness_column_witness) + (eri_bit_etc_etcc_column_count_semantic_prefix_witness_column_witness_row))) /\ (((eri_bit_etc_etcc_column_count_semantic_prefix_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_choice_left. eri_gap_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_column_count_semantic_prefix_witness_column) = q * S eri_column_etc_etcc_column_count_semantic_prefix_witness_column_witness_row) /\ ~(exists eri_gap_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_choice_right. eri_gap_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_column_count_semantic_prefix_witness_column_witness_row) = p * S etc_row_index_etcc_column_count_semantic_prefix_witness_column))) \/ (eri_bit_etc_etcc_column_count_semantic_prefix_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_choice_right. eri_gap_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_column_count_semantic_prefix_witness_column_witness_row) = p * S etc_row_index_etcc_column_count_semantic_prefix_witness_column) /\ ~(exists eri_gap_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_choice_left. eri_gap_etc_etcc_column_count_semantic_prefix_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_column_count_semantic_prefix_witness_column) = q * S eri_column_etc_etcc_column_count_semantic_prefix_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum ff_v_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_start. ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_start. ff_u_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_terminal. ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_terminal + S (etc_count_etcc_column_count_semantic_prefix_witness_column_witness) = S ((S (h)) * ff_v_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_terminal. ff_u_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum) + (etc_count_etcc_column_count_semantic_prefix_witness_column_witness))) /\ forall ff_i_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum. (exists ff_lt_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_bound. ff_lt_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_bound + S ff_i_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum = h) -> exists ff_a_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum ff_r_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum ff_s_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_summand. ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_column_count_semantic_prefix_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_summand. etc_row_code_etcc_column_count_semantic_prefix_witness_column_witness = ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_column_count_semantic_prefix_witness_column_witness) + (ff_a_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_partial. ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_partial. ff_u_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum) + (ff_r_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_successor. ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_successor. ff_u_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum) + (ff_s_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum))) /\ ff_s_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum = ff_r_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum + ff_a_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits. (exists ff_lt_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits_bound. ff_lt_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits_bound + S ff_i_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits = h) -> exists ff_bit_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits_decoded. ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_column_count_semantic_prefix_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits_decoded. etc_row_code_etcc_column_count_semantic_prefix_witness_column_witness = ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_column_count_semantic_prefix_witness_column_witness) + (ff_bit_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_etcc_column_count_semantic_prefix_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_inner_entry. ff_h_etc_etcc_column_count_semantic_prefix_witness_column_witness_inner_entry + S (etc_bit_etcc_column_count_semantic_prefix_witness_column) = S ((S (etcc_row_index_column_count_semantic_prefix)) * etc_row_scale_etcc_column_count_semantic_prefix_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_inner_entry. etc_row_code_etcc_column_count_semantic_prefix_witness_column_witness = ff_q_etc_etcc_column_count_semantic_prefix_witness_column_witness_inner_entry * S ((S (etcc_row_index_column_count_semantic_prefix)) * etc_row_scale_etcc_column_count_semantic_prefix_witness_column_witness) + (etc_bit_etcc_column_count_semantic_prefix_witness_column)))))))) /\ ((((exists ff_u_etcc_column_count_semantic_prefix_witness_column_count_sum ff_v_etcc_column_count_semantic_prefix_witness_column_count_sum. ((((exists ff_h_etcc_column_count_semantic_prefix_witness_column_count_sum_start. ff_h_etcc_column_count_semantic_prefix_witness_column_count_sum_start + S (0) = S ((S (0)) * ff_v_etcc_column_count_semantic_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_semantic_prefix_witness_column_count_sum_start. ff_u_etcc_column_count_semantic_prefix_witness_column_count_sum = ff_q_etcc_column_count_semantic_prefix_witness_column_count_sum_start * S ((S (0)) * ff_v_etcc_column_count_semantic_prefix_witness_column_count_sum) + (0))) /\ ((((exists ff_h_etcc_column_count_semantic_prefix_witness_column_count_sum_terminal. ff_h_etcc_column_count_semantic_prefix_witness_column_count_sum_terminal + S (etcc_count_column_count_semantic_prefix) = S ((S (k)) * ff_v_etcc_column_count_semantic_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_semantic_prefix_witness_column_count_sum_terminal. ff_u_etcc_column_count_semantic_prefix_witness_column_count_sum = ff_q_etcc_column_count_semantic_prefix_witness_column_count_sum_terminal * S ((S (k)) * ff_v_etcc_column_count_semantic_prefix_witness_column_count_sum) + (etcc_count_column_count_semantic_prefix))) /\ forall ff_i_etcc_column_count_semantic_prefix_witness_column_count_sum. (exists ff_lt_etcc_column_count_semantic_prefix_witness_column_count_sum_bound. ff_lt_etcc_column_count_semantic_prefix_witness_column_count_sum_bound + S ff_i_etcc_column_count_semantic_prefix_witness_column_count_sum = k) -> exists ff_a_etcc_column_count_semantic_prefix_witness_column_count_sum ff_r_etcc_column_count_semantic_prefix_witness_column_count_sum ff_s_etcc_column_count_semantic_prefix_witness_column_count_sum. ((((exists ff_h_etcc_column_count_semantic_prefix_witness_column_count_sum_summand. ff_h_etcc_column_count_semantic_prefix_witness_column_count_sum_summand + S (ff_a_etcc_column_count_semantic_prefix_witness_column_count_sum) = S ((S (ff_i_etcc_column_count_semantic_prefix_witness_column_count_sum)) * etcc_column_scale_column_count_semantic_prefix_witness)) /\ exists ff_q_etcc_column_count_semantic_prefix_witness_column_count_sum_summand. etcc_column_code_column_count_semantic_prefix_witness = ff_q_etcc_column_count_semantic_prefix_witness_column_count_sum_summand * S ((S (ff_i_etcc_column_count_semantic_prefix_witness_column_count_sum)) * etcc_column_scale_column_count_semantic_prefix_witness) + (ff_a_etcc_column_count_semantic_prefix_witness_column_count_sum))) /\ ((((exists ff_h_etcc_column_count_semantic_prefix_witness_column_count_sum_partial. ff_h_etcc_column_count_semantic_prefix_witness_column_count_sum_partial + S (ff_r_etcc_column_count_semantic_prefix_witness_column_count_sum) = S ((S (ff_i_etcc_column_count_semantic_prefix_witness_column_count_sum)) * ff_v_etcc_column_count_semantic_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_semantic_prefix_witness_column_count_sum_partial. ff_u_etcc_column_count_semantic_prefix_witness_column_count_sum = ff_q_etcc_column_count_semantic_prefix_witness_column_count_sum_partial * S ((S (ff_i_etcc_column_count_semantic_prefix_witness_column_count_sum)) * ff_v_etcc_column_count_semantic_prefix_witness_column_count_sum) + (ff_r_etcc_column_count_semantic_prefix_witness_column_count_sum))) /\ ((((exists ff_h_etcc_column_count_semantic_prefix_witness_column_count_sum_successor. ff_h_etcc_column_count_semantic_prefix_witness_column_count_sum_successor + S (ff_s_etcc_column_count_semantic_prefix_witness_column_count_sum) = S ((S (S ff_i_etcc_column_count_semantic_prefix_witness_column_count_sum)) * ff_v_etcc_column_count_semantic_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_semantic_prefix_witness_column_count_sum_successor. ff_u_etcc_column_count_semantic_prefix_witness_column_count_sum = ff_q_etcc_column_count_semantic_prefix_witness_column_count_sum_successor * S ((S (S ff_i_etcc_column_count_semantic_prefix_witness_column_count_sum)) * ff_v_etcc_column_count_semantic_prefix_witness_column_count_sum) + (ff_s_etcc_column_count_semantic_prefix_witness_column_count_sum))) /\ ff_s_etcc_column_count_semantic_prefix_witness_column_count_sum = ff_r_etcc_column_count_semantic_prefix_witness_column_count_sum + ff_a_etcc_column_count_semantic_prefix_witness_column_count_sum)))))) /\ (forall ff_i_etcc_column_count_semantic_prefix_witness_column_count_bits. (exists ff_lt_etcc_column_count_semantic_prefix_witness_column_count_bits_bound. ff_lt_etcc_column_count_semantic_prefix_witness_column_count_bits_bound + S ff_i_etcc_column_count_semantic_prefix_witness_column_count_bits = k) -> exists ff_bit_etcc_column_count_semantic_prefix_witness_column_count_bits. ((((exists ff_h_etcc_column_count_semantic_prefix_witness_column_count_bits_decoded. ff_h_etcc_column_count_semantic_prefix_witness_column_count_bits_decoded + S (ff_bit_etcc_column_count_semantic_prefix_witness_column_count_bits) = S ((S (ff_i_etcc_column_count_semantic_prefix_witness_column_count_bits)) * etcc_column_scale_column_count_semantic_prefix_witness)) /\ exists ff_q_etcc_column_count_semantic_prefix_witness_column_count_bits_decoded. etcc_column_code_column_count_semantic_prefix_witness = ff_q_etcc_column_count_semantic_prefix_witness_column_count_bits_decoded * S ((S (ff_i_etcc_column_count_semantic_prefix_witness_column_count_bits)) * etcc_column_scale_column_count_semantic_prefix_witness) + (ff_bit_etcc_column_count_semantic_prefix_witness_column_count_bits))) /\ (ff_bit_etcc_column_count_semantic_prefix_witness_column_count_bits = 0 \/ ff_bit_etcc_column_count_semantic_prefix_witness_column_count_bits = 1))))) /\ etcc_row_count_column_count_semantic_prefix_witness + etcc_count_column_count_semantic_prefix = k))))) -> (exists edt_lt_gap_column_count_row_bound. edt_lt_gap_column_count_row_bound + S (i) = h) -> (((exists ff_h_column_count_first_entry. ff_h_column_count_first_entry + S (n) = S ((S (i)) * ac)) /\ exists ff_q_column_count_first_entry. ab = ff_q_column_count_first_entry * S ((S (i)) * ac) + (n))) -> (((exists ff_h_column_count_decoded_entry. ff_h_column_count_decoded_entry + S (m) = S ((S (i)) * dc)) /\ exists ff_q_column_count_decoded_entry. db = ff_q_column_count_decoded_entry * S ((S (i)) * dc) + (m))) -> n + m = k

Structural proof guide

Generated structural guide

Decoded original-row and constructed-column counts partition the row width.

Use the direct prerequisites eisenstein_transposed_column_count_decoded_witness, beta_at_unique as previously established PA formulas.

The proof proceeds by case analysis (7), intermediate claims (2), equality transport (1).

Referenced ingredients

PA00EM eisenstein_transposed_column_count_decoded_witness PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA00EM eisenstein_transposed_column_count_decoded_witness PA002F beta_at_unique

Direct dependents

PA00EO eisenstein_transposed_column_count_matches_decoded_constant

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

52 script commands · 7 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.

Named ingredients (2)
eisenstein transposed column count decoded witnessbeta at unique

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 h
  4. L4
    intro k
  5. L5
    intro ab
  6. L6
    intro ac
  7. L7
    intro bb
  8. L8
    intro bc
  9. L9
    intro db
  10. L10
    intro dc
02Fix variables and assumptionsL11–17

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

  1. L11
    intro i
  2. L12
    intro n
  3. L13
    intro m
  4. L14
    intro hprefix
  5. L15
    intro hi
  6. L16
    intro hn
  7. L17
    intro hm
03Establish hwitnessL18–27

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

  1. L18
    have hwitness · expand full local formula (968 characters)have hwitness : ∃ etcc_row_count_column_count_decoded_witness. ∃ etcc_column_code_column_count_decoded_witness. ∃ etcc_column_scale_column_count_decoded_witness. BetaAt(ab,ac,i,etcc_row_count_column_count_decoded_witness) ∧ (∃ x. ∃ y. (∀ z. Lt(z,k) → ∃ n. BetaAt(x,y,z,n) ∧ (n = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ n = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))) ∧ BitCount(x,y,k,etcc_row_count_column_count_decoded_witness)) ∧ (∀ x. Lt(x,k) → ∃ y. BetaAt(etcc_column_code_column_count_decoded_witness,etcc_column_scale_column_count_decoded_witness,x,y) ∧ (∃ z. ∃ n. ∃ j. BetaAt(bb,bc,x,z) ∧ (∀ u. Lt(u,h) → ∃ v. BetaAt(n,j,u,v) ∧ (v = 0 ∧ (Lt(p · S x,q · S u) ∧ ¬Lt(q · S u,p · S x)) ∨ v = 1 ∧ (Lt(q · S u,p · S x) ∧ ¬Lt(p · S x,q · S u)))) ∧ BitCount(n,j,h,z) ∧ BetaAt(n,j,i,y))) ∧ (BitCount(etcc_column_code_column_count_decoded_witness,etcc_column_scale_column_count_decoded_witness,k,m) ∧ etcc_row_count_column_count_decoded_witness + m = k)
    Definitions: LtBetaAtBitCount
  2. L19
    specialize eisenstein_transposed_column_count_decoded_witness p
  3. L20
    specialize eisenstein_transposed_column_count_decoded_witness q
  4. L21
    specialize eisenstein_transposed_column_count_decoded_witness h
  5. L22
    specialize eisenstein_transposed_column_count_decoded_witness k
  6. L23
    specialize eisenstein_transposed_column_count_decoded_witness ab
  7. L24
    specialize eisenstein_transposed_column_count_decoded_witness ac
  8. L25
    specialize eisenstein_transposed_column_count_decoded_witness bb
  9. L26
    specialize eisenstein_transposed_column_count_decoded_witness bc
  10. L27
    specialize eisenstein_transposed_column_count_decoded_witness db
04Use earlier factsL28–34

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

  1. L28
    specialize eisenstein_transposed_column_count_decoded_witness dc
  2. L29
    specialize eisenstein_transposed_column_count_decoded_witness i
  3. L30
    specialize eisenstein_transposed_column_count_decoded_witness m
  4. L31
    apply eisenstein_transposed_column_count_decoded_witness
  5. L32
    exact hprefix
  6. L33
    exact hi
  7. L34
    exact hm
05Separate the logical casesL35–41

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

  1. L35
    cases hwitness
  2. L36
    cases hwitness_witness
  3. L37
    cases hwitness_witness_witness
  4. L38
    cases hwitness_witness_witness_witness
  5. L39
    cases hwitness_witness_witness_witness_left
  6. L40
    cases hwitness_witness_witness_witness_left_left
  7. L41
    cases hwitness_witness_witness_witness_right
06Establish hroweqL42–51

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

  1. L42
    have hroweq : x = n
  2. L43
    specialize beta_at_unique ab
  3. L44
    specialize beta_at_unique ac
  4. L45
    specialize beta_at_unique i
  5. L46
    specialize beta_at_unique x
  6. L47
    specialize beta_at_unique n
  7. L48
    apply beta_at_unique
  8. L49
    exact hwitness_witness_witness_witness_left_left_left
  9. L50
    exact hn
  10. L51
    rewrite hroweq at hwitness_witness_witness_witness_right_right
07Use earlier factsL52–52

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

  1. L52
    exact hwitness_witness_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 52 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 db
  10. 0010intro dc
  11. 0011intro i
  12. 0012intro n
  13. 0013intro m
  14. 0014intro hprefix
  15. 0015intro hi
  16. 0016intro hn
  17. 0017intro hm
  18. 0018have hwitness : exists etcc_row_count_column_count_decoded_witness etcc_column_code_column_count_decoded_witness etcc_column_scale_column_count_decoded_witness. ((((((exists ff_h_etcc_column_count_decoded_witness_first_entry. ff_h_etcc_column_count_decoded_witness_first_entry + S (etcc_row_count_column_count_decoded_witness) = S ((S (i)) * ac)) /\ exists ff_q_etcc_column_count_decoded_witness_first_entry. ab = ff_q_etcc_column_count_decoded_witness_first_entry * S ((S (i)) * ac) + (etcc_row_count_column_count_decoded_witness))) /\ (exists erc_row_code_etcc_column_count_decoded_witness_row_semantics erc_row_scale_etcc_column_count_decoded_witness_row_semantics. ((forall eri_column_erc_etcc_column_count_decoded_witness_row_semantics_row. (exists eri_gap_erc_etcc_column_count_decoded_witness_row_semantics_row_bound. eri_gap_erc_etcc_column_count_decoded_witness_row_semantics_row_bound + S (eri_column_erc_etcc_column_count_decoded_witness_row_semantics_row) = k) -> exists eri_bit_erc_etcc_column_count_decoded_witness_row_semantics_row. ((((exists ff_h_eri_erc_etcc_column_count_decoded_witness_row_semantics_row_decoded. ff_h_eri_erc_etcc_column_count_decoded_witness_row_semantics_row_decoded + S (eri_bit_erc_etcc_column_count_decoded_witness_row_semantics_row) = S ((S (eri_column_erc_etcc_column_count_decoded_witness_row_semantics_row)) * erc_row_scale_etcc_column_count_decoded_witness_row_semantics)) /\ exists ff_q_eri_erc_etcc_column_count_decoded_witness_row_semantics_row_decoded. erc_row_code_etcc_column_count_decoded_witness_row_semantics = ff_q_eri_erc_etcc_column_count_decoded_witness_row_semantics_row_decoded * S ((S (eri_column_erc_etcc_column_count_decoded_witness_row_semantics_row)) * erc_row_scale_etcc_column_count_decoded_witness_row_semantics) + (eri_bit_erc_etcc_column_count_decoded_witness_row_semantics_row))) /\ (((eri_bit_erc_etcc_column_count_decoded_witness_row_semantics_row = 0 /\ ((exists eri_gap_erc_etcc_column_count_decoded_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_column_count_decoded_witness_row_semantics_row_choice_left + S (q * S i) = p * S eri_column_erc_etcc_column_count_decoded_witness_row_semantics_row) /\ ~(exists eri_gap_erc_etcc_column_count_decoded_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_column_count_decoded_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_column_count_decoded_witness_row_semantics_row) = q * S i))) \/ (eri_bit_erc_etcc_column_count_decoded_witness_row_semantics_row = 1 /\ ((exists eri_gap_erc_etcc_column_count_decoded_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_column_count_decoded_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_column_count_decoded_witness_row_semantics_row) = q * S i) /\ ~(exists eri_gap_erc_etcc_column_count_decoded_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_column_count_decoded_witness_row_semantics_row_choice_left + S (q * S i) = p * S eri_column_erc_etcc_column_count_decoded_witness_row_semantics_row))))))) /\ (((exists ff_u_erc_etcc_column_count_decoded_witness_row_semantics_count_sum ff_v_erc_etcc_column_count_decoded_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_start. ff_h_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_etcc_column_count_decoded_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_start. ff_u_erc_etcc_column_count_decoded_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_start * S ((S (0)) * ff_v_erc_etcc_column_count_decoded_witness_row_semantics_count_sum) + (0))) /\ ((((exists ff_h_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_terminal. ff_h_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_terminal + S (etcc_row_count_column_count_decoded_witness) = S ((S (k)) * ff_v_erc_etcc_column_count_decoded_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_terminal. ff_u_erc_etcc_column_count_decoded_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_terminal * S ((S (k)) * ff_v_erc_etcc_column_count_decoded_witness_row_semantics_count_sum) + (etcc_row_count_column_count_decoded_witness))) /\ forall ff_i_erc_etcc_column_count_decoded_witness_row_semantics_count_sum. (exists ff_lt_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_bound. ff_lt_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_bound + S ff_i_erc_etcc_column_count_decoded_witness_row_semantics_count_sum = k) -> exists ff_a_erc_etcc_column_count_decoded_witness_row_semantics_count_sum ff_r_erc_etcc_column_count_decoded_witness_row_semantics_count_sum ff_s_erc_etcc_column_count_decoded_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_summand. ff_h_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_summand + S (ff_a_erc_etcc_column_count_decoded_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_column_count_decoded_witness_row_semantics_count_sum)) * erc_row_scale_etcc_column_count_decoded_witness_row_semantics)) /\ exists ff_q_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_summand. erc_row_code_etcc_column_count_decoded_witness_row_semantics = ff_q_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_summand * S ((S (ff_i_erc_etcc_column_count_decoded_witness_row_semantics_count_sum)) * erc_row_scale_etcc_column_count_decoded_witness_row_semantics) + (ff_a_erc_etcc_column_count_decoded_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_partial. ff_h_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_partial + S (ff_r_erc_etcc_column_count_decoded_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_column_count_decoded_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_decoded_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_partial. ff_u_erc_etcc_column_count_decoded_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_partial * S ((S (ff_i_erc_etcc_column_count_decoded_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_decoded_witness_row_semantics_count_sum) + (ff_r_erc_etcc_column_count_decoded_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_successor. ff_h_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_successor + S (ff_s_erc_etcc_column_count_decoded_witness_row_semantics_count_sum) = S ((S (S ff_i_erc_etcc_column_count_decoded_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_decoded_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_successor. ff_u_erc_etcc_column_count_decoded_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_decoded_witness_row_semantics_count_sum_successor * S ((S (S ff_i_erc_etcc_column_count_decoded_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_decoded_witness_row_semantics_count_sum) + (ff_s_erc_etcc_column_count_decoded_witness_row_semantics_count_sum))) /\ ff_s_erc_etcc_column_count_decoded_witness_row_semantics_count_sum = ff_r_erc_etcc_column_count_decoded_witness_row_semantics_count_sum + ff_a_erc_etcc_column_count_decoded_witness_row_semantics_count_sum)))))) /\ (forall ff_i_erc_etcc_column_count_decoded_witness_row_semantics_count_bits. (exists ff_lt_erc_etcc_column_count_decoded_witness_row_semantics_count_bits_bound. ff_lt_erc_etcc_column_count_decoded_witness_row_semantics_count_bits_bound + S ff_i_erc_etcc_column_count_decoded_witness_row_semantics_count_bits = k) -> exists ff_bit_erc_etcc_column_count_decoded_witness_row_semantics_count_bits. ((((exists ff_h_erc_etcc_column_count_decoded_witness_row_semantics_count_bits_decoded. ff_h_erc_etcc_column_count_decoded_witness_row_semantics_count_bits_decoded + S (ff_bit_erc_etcc_column_count_decoded_witness_row_semantics_count_bits) = S ((S (ff_i_erc_etcc_column_count_decoded_witness_row_semantics_count_bits)) * erc_row_scale_etcc_column_count_decoded_witness_row_semantics)) /\ exists ff_q_erc_etcc_column_count_decoded_witness_row_semantics_count_bits_decoded. erc_row_code_etcc_column_count_decoded_witness_row_semantics = ff_q_erc_etcc_column_count_decoded_witness_row_semantics_count_bits_decoded * S ((S (ff_i_erc_etcc_column_count_decoded_witness_row_semantics_count_bits)) * erc_row_scale_etcc_column_count_decoded_witness_row_semantics) + (ff_bit_erc_etcc_column_count_decoded_witness_row_semantics_count_bits))) /\ (ff_bit_erc_etcc_column_count_decoded_witness_row_semantics_count_bits = 0 \/ ff_bit_erc_etcc_column_count_decoded_witness_row_semantics_count_bits = 1)))))))) /\ (forall etc_row_index_etcc_column_count_decoded_witness_column. (exists edt_lt_gap_etcc_column_count_decoded_witness_column_bound. edt_lt_gap_etcc_column_count_decoded_witness_column_bound + S (etc_row_index_etcc_column_count_decoded_witness_column) = k) -> exists etc_bit_etcc_column_count_decoded_witness_column. ((((exists ff_h_etc_etcc_column_count_decoded_witness_column_decoded. ff_h_etc_etcc_column_count_decoded_witness_column_decoded + S (etc_bit_etcc_column_count_decoded_witness_column) = S ((S (etc_row_index_etcc_column_count_decoded_witness_column)) * etcc_column_scale_column_count_decoded_witness)) /\ exists ff_q_etc_etcc_column_count_decoded_witness_column_decoded. etcc_column_code_column_count_decoded_witness = ff_q_etc_etcc_column_count_decoded_witness_column_decoded * S ((S (etc_row_index_etcc_column_count_decoded_witness_column)) * etcc_column_scale_column_count_decoded_witness) + (etc_bit_etcc_column_count_decoded_witness_column))) /\ (exists etc_count_etcc_column_count_decoded_witness_column_witness etc_row_code_etcc_column_count_decoded_witness_column_witness etc_row_scale_etcc_column_count_decoded_witness_column_witness. ((((((exists ff_h_etc_etcc_column_count_decoded_witness_column_witness_outer_entry. ff_h_etc_etcc_column_count_decoded_witness_column_witness_outer_entry + S (etc_count_etcc_column_count_decoded_witness_column_witness) = S ((S (etc_row_index_etcc_column_count_decoded_witness_column)) * bc)) /\ exists ff_q_etc_etcc_column_count_decoded_witness_column_witness_outer_entry. bb = ff_q_etc_etcc_column_count_decoded_witness_column_witness_outer_entry * S ((S (etc_row_index_etcc_column_count_decoded_witness_column)) * bc) + (etc_count_etcc_column_count_decoded_witness_column_witness))) /\ (forall eri_column_etc_etcc_column_count_decoded_witness_column_witness_row. (exists eri_gap_etc_etcc_column_count_decoded_witness_column_witness_row_bound. eri_gap_etc_etcc_column_count_decoded_witness_column_witness_row_bound + S (eri_column_etc_etcc_column_count_decoded_witness_column_witness_row) = h) -> exists eri_bit_etc_etcc_column_count_decoded_witness_column_witness_row. ((((exists ff_h_eri_etc_etcc_column_count_decoded_witness_column_witness_row_decoded. ff_h_eri_etc_etcc_column_count_decoded_witness_column_witness_row_decoded + S (eri_bit_etc_etcc_column_count_decoded_witness_column_witness_row) = S ((S (eri_column_etc_etcc_column_count_decoded_witness_column_witness_row)) * etc_row_scale_etcc_column_count_decoded_witness_column_witness)) /\ exists ff_q_eri_etc_etcc_column_count_decoded_witness_column_witness_row_decoded. etc_row_code_etcc_column_count_decoded_witness_column_witness = ff_q_eri_etc_etcc_column_count_decoded_witness_column_witness_row_decoded * S ((S (eri_column_etc_etcc_column_count_decoded_witness_column_witness_row)) * etc_row_scale_etcc_column_count_decoded_witness_column_witness) + (eri_bit_etc_etcc_column_count_decoded_witness_column_witness_row))) /\ (((eri_bit_etc_etcc_column_count_decoded_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_etcc_column_count_decoded_witness_column_witness_row_choice_left. eri_gap_etc_etcc_column_count_decoded_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_column_count_decoded_witness_column) = q * S eri_column_etc_etcc_column_count_decoded_witness_column_witness_row) /\ ~(exists eri_gap_etc_etcc_column_count_decoded_witness_column_witness_row_choice_right. eri_gap_etc_etcc_column_count_decoded_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_column_count_decoded_witness_column_witness_row) = p * S etc_row_index_etcc_column_count_decoded_witness_column))) \/ (eri_bit_etc_etcc_column_count_decoded_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_etcc_column_count_decoded_witness_column_witness_row_choice_right. eri_gap_etc_etcc_column_count_decoded_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_column_count_decoded_witness_column_witness_row) = p * S etc_row_index_etcc_column_count_decoded_witness_column) /\ ~(exists eri_gap_etc_etcc_column_count_decoded_witness_column_witness_row_choice_left. eri_gap_etc_etcc_column_count_decoded_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_column_count_decoded_witness_column) = q * S eri_column_etc_etcc_column_count_decoded_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum ff_v_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_start. ff_h_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_start. ff_u_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_terminal. ff_h_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_terminal + S (etc_count_etcc_column_count_decoded_witness_column_witness) = S ((S (h)) * ff_v_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_terminal. ff_u_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum) + (etc_count_etcc_column_count_decoded_witness_column_witness))) /\ forall ff_i_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum. (exists ff_lt_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_bound. ff_lt_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_bound + S ff_i_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum = h) -> exists ff_a_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum ff_r_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum ff_s_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_summand. ff_h_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_column_count_decoded_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_summand. etc_row_code_etcc_column_count_decoded_witness_column_witness = ff_q_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_column_count_decoded_witness_column_witness) + (ff_a_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_partial. ff_h_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_partial. ff_u_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum) + (ff_r_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_successor. ff_h_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_successor. ff_u_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum) + (ff_s_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum))) /\ ff_s_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum = ff_r_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum + ff_a_etc_etcc_column_count_decoded_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits. (exists ff_lt_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits_bound. ff_lt_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits_bound + S ff_i_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits = h) -> exists ff_bit_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits_decoded. ff_h_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_column_count_decoded_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits_decoded. etc_row_code_etcc_column_count_decoded_witness_column_witness = ff_q_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_column_count_decoded_witness_column_witness) + (ff_bit_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_etcc_column_count_decoded_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_etcc_column_count_decoded_witness_column_witness_inner_entry. ff_h_etc_etcc_column_count_decoded_witness_column_witness_inner_entry + S (etc_bit_etcc_column_count_decoded_witness_column) = S ((S (i)) * etc_row_scale_etcc_column_count_decoded_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_decoded_witness_column_witness_inner_entry. etc_row_code_etcc_column_count_decoded_witness_column_witness = ff_q_etc_etcc_column_count_decoded_witness_column_witness_inner_entry * S ((S (i)) * etc_row_scale_etcc_column_count_decoded_witness_column_witness) + (etc_bit_etcc_column_count_decoded_witness_column)))))))) /\ ((((exists ff_u_etcc_column_count_decoded_witness_column_count_sum ff_v_etcc_column_count_decoded_witness_column_count_sum. ((((exists ff_h_etcc_column_count_decoded_witness_column_count_sum_start. ff_h_etcc_column_count_decoded_witness_column_count_sum_start + S (0) = S ((S (0)) * ff_v_etcc_column_count_decoded_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_decoded_witness_column_count_sum_start. ff_u_etcc_column_count_decoded_witness_column_count_sum = ff_q_etcc_column_count_decoded_witness_column_count_sum_start * S ((S (0)) * ff_v_etcc_column_count_decoded_witness_column_count_sum) + (0))) /\ ((((exists ff_h_etcc_column_count_decoded_witness_column_count_sum_terminal. ff_h_etcc_column_count_decoded_witness_column_count_sum_terminal + S (m) = S ((S (k)) * ff_v_etcc_column_count_decoded_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_decoded_witness_column_count_sum_terminal. ff_u_etcc_column_count_decoded_witness_column_count_sum = ff_q_etcc_column_count_decoded_witness_column_count_sum_terminal * S ((S (k)) * ff_v_etcc_column_count_decoded_witness_column_count_sum) + (m))) /\ forall ff_i_etcc_column_count_decoded_witness_column_count_sum. (exists ff_lt_etcc_column_count_decoded_witness_column_count_sum_bound. ff_lt_etcc_column_count_decoded_witness_column_count_sum_bound + S ff_i_etcc_column_count_decoded_witness_column_count_sum = k) -> exists ff_a_etcc_column_count_decoded_witness_column_count_sum ff_r_etcc_column_count_decoded_witness_column_count_sum ff_s_etcc_column_count_decoded_witness_column_count_sum. ((((exists ff_h_etcc_column_count_decoded_witness_column_count_sum_summand. ff_h_etcc_column_count_decoded_witness_column_count_sum_summand + S (ff_a_etcc_column_count_decoded_witness_column_count_sum) = S ((S (ff_i_etcc_column_count_decoded_witness_column_count_sum)) * etcc_column_scale_column_count_decoded_witness)) /\ exists ff_q_etcc_column_count_decoded_witness_column_count_sum_summand. etcc_column_code_column_count_decoded_witness = ff_q_etcc_column_count_decoded_witness_column_count_sum_summand * S ((S (ff_i_etcc_column_count_decoded_witness_column_count_sum)) * etcc_column_scale_column_count_decoded_witness) + (ff_a_etcc_column_count_decoded_witness_column_count_sum))) /\ ((((exists ff_h_etcc_column_count_decoded_witness_column_count_sum_partial. ff_h_etcc_column_count_decoded_witness_column_count_sum_partial + S (ff_r_etcc_column_count_decoded_witness_column_count_sum) = S ((S (ff_i_etcc_column_count_decoded_witness_column_count_sum)) * ff_v_etcc_column_count_decoded_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_decoded_witness_column_count_sum_partial. ff_u_etcc_column_count_decoded_witness_column_count_sum = ff_q_etcc_column_count_decoded_witness_column_count_sum_partial * S ((S (ff_i_etcc_column_count_decoded_witness_column_count_sum)) * ff_v_etcc_column_count_decoded_witness_column_count_sum) + (ff_r_etcc_column_count_decoded_witness_column_count_sum))) /\ ((((exists ff_h_etcc_column_count_decoded_witness_column_count_sum_successor. ff_h_etcc_column_count_decoded_witness_column_count_sum_successor + S (ff_s_etcc_column_count_decoded_witness_column_count_sum) = S ((S (S ff_i_etcc_column_count_decoded_witness_column_count_sum)) * ff_v_etcc_column_count_decoded_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_decoded_witness_column_count_sum_successor. ff_u_etcc_column_count_decoded_witness_column_count_sum = ff_q_etcc_column_count_decoded_witness_column_count_sum_successor * S ((S (S ff_i_etcc_column_count_decoded_witness_column_count_sum)) * ff_v_etcc_column_count_decoded_witness_column_count_sum) + (ff_s_etcc_column_count_decoded_witness_column_count_sum))) /\ ff_s_etcc_column_count_decoded_witness_column_count_sum = ff_r_etcc_column_count_decoded_witness_column_count_sum + ff_a_etcc_column_count_decoded_witness_column_count_sum)))))) /\ (forall ff_i_etcc_column_count_decoded_witness_column_count_bits. (exists ff_lt_etcc_column_count_decoded_witness_column_count_bits_bound. ff_lt_etcc_column_count_decoded_witness_column_count_bits_bound + S ff_i_etcc_column_count_decoded_witness_column_count_bits = k) -> exists ff_bit_etcc_column_count_decoded_witness_column_count_bits. ((((exists ff_h_etcc_column_count_decoded_witness_column_count_bits_decoded. ff_h_etcc_column_count_decoded_witness_column_count_bits_decoded + S (ff_bit_etcc_column_count_decoded_witness_column_count_bits) = S ((S (ff_i_etcc_column_count_decoded_witness_column_count_bits)) * etcc_column_scale_column_count_decoded_witness)) /\ exists ff_q_etcc_column_count_decoded_witness_column_count_bits_decoded. etcc_column_code_column_count_decoded_witness = ff_q_etcc_column_count_decoded_witness_column_count_bits_decoded * S ((S (ff_i_etcc_column_count_decoded_witness_column_count_bits)) * etcc_column_scale_column_count_decoded_witness) + (ff_bit_etcc_column_count_decoded_witness_column_count_bits))) /\ (ff_bit_etcc_column_count_decoded_witness_column_count_bits = 0 \/ ff_bit_etcc_column_count_decoded_witness_column_count_bits = 1))))) /\ etcc_row_count_column_count_decoded_witness + m = k))
  19. 0019specialize eisenstein_transposed_column_count_decoded_witness p
  20. 0020specialize eisenstein_transposed_column_count_decoded_witness q
  21. 0021specialize eisenstein_transposed_column_count_decoded_witness h
  22. 0022specialize eisenstein_transposed_column_count_decoded_witness k
  23. 0023specialize eisenstein_transposed_column_count_decoded_witness ab
  24. 0024specialize eisenstein_transposed_column_count_decoded_witness ac
  25. 0025specialize eisenstein_transposed_column_count_decoded_witness bb
  26. 0026specialize eisenstein_transposed_column_count_decoded_witness bc
  27. 0027specialize eisenstein_transposed_column_count_decoded_witness db
  28. 0028specialize eisenstein_transposed_column_count_decoded_witness dc
  29. 0029specialize eisenstein_transposed_column_count_decoded_witness i
  30. 0030specialize eisenstein_transposed_column_count_decoded_witness m
  31. 0031apply eisenstein_transposed_column_count_decoded_witness
  32. 0032exact hprefix
  33. 0033exact hi
  34. 0034exact hm
  35. 0035cases hwitness
  36. 0036cases hwitness_witness
  37. 0037cases hwitness_witness_witness
  38. 0038cases hwitness_witness_witness_witness
  39. 0039cases hwitness_witness_witness_witness_left
  40. 0040cases hwitness_witness_witness_witness_left_left
  41. 0041cases hwitness_witness_witness_witness_right
  42. 0042have hroweq : x = n
  43. 0043specialize beta_at_unique ab
  44. 0044specialize beta_at_unique ac
  45. 0045specialize beta_at_unique i
  46. 0046specialize beta_at_unique x
  47. 0047specialize beta_at_unique n
  48. 0048apply beta_at_unique
  49. 0049exact hwitness_witness_witness_witness_left_left_left
  50. 0050exact hn
  51. 0051rewrite hroweq at hwitness_witness_witness_witness_right_right
  52. 0052exact hwitness_witness_witness_witness_right_right