PA00E8

eisenstein_transposed_column_prefix_extend

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

Append one provenance-carrying swapped-row bit to a transposed column.

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 bb bc i z e l. (forall etc_row_index_transposed_column_extend_before. (exists edt_lt_gap_transposed_column_extend_before_bound. edt_lt_gap_transposed_column_extend_before_bound + S (etc_row_index_transposed_column_extend_before) = l) -> exists etc_bit_transposed_column_extend_before. ((((exists ff_h_etc_transposed_column_extend_before_decoded. ff_h_etc_transposed_column_extend_before_decoded + S (etc_bit_transposed_column_extend_before) = S ((S (etc_row_index_transposed_column_extend_before)) * e)) /\ exists ff_q_etc_transposed_column_extend_before_decoded. z = ff_q_etc_transposed_column_extend_before_decoded * S ((S (etc_row_index_transposed_column_extend_before)) * e) + (etc_bit_transposed_column_extend_before))) /\ (exists etc_count_transposed_column_extend_before_witness etc_row_code_transposed_column_extend_before_witness etc_row_scale_transposed_column_extend_before_witness. ((((((exists ff_h_etc_transposed_column_extend_before_witness_outer_entry. ff_h_etc_transposed_column_extend_before_witness_outer_entry + S (etc_count_transposed_column_extend_before_witness) = S ((S (etc_row_index_transposed_column_extend_before)) * bc)) /\ exists ff_q_etc_transposed_column_extend_before_witness_outer_entry. bb = ff_q_etc_transposed_column_extend_before_witness_outer_entry * S ((S (etc_row_index_transposed_column_extend_before)) * bc) + (etc_count_transposed_column_extend_before_witness))) /\ (forall eri_column_etc_transposed_column_extend_before_witness_row. (exists eri_gap_etc_transposed_column_extend_before_witness_row_bound. eri_gap_etc_transposed_column_extend_before_witness_row_bound + S (eri_column_etc_transposed_column_extend_before_witness_row) = h) -> exists eri_bit_etc_transposed_column_extend_before_witness_row. ((((exists ff_h_eri_etc_transposed_column_extend_before_witness_row_decoded. ff_h_eri_etc_transposed_column_extend_before_witness_row_decoded + S (eri_bit_etc_transposed_column_extend_before_witness_row) = S ((S (eri_column_etc_transposed_column_extend_before_witness_row)) * etc_row_scale_transposed_column_extend_before_witness)) /\ exists ff_q_eri_etc_transposed_column_extend_before_witness_row_decoded. etc_row_code_transposed_column_extend_before_witness = ff_q_eri_etc_transposed_column_extend_before_witness_row_decoded * S ((S (eri_column_etc_transposed_column_extend_before_witness_row)) * etc_row_scale_transposed_column_extend_before_witness) + (eri_bit_etc_transposed_column_extend_before_witness_row))) /\ (((eri_bit_etc_transposed_column_extend_before_witness_row = 0 /\ ((exists eri_gap_etc_transposed_column_extend_before_witness_row_choice_left. eri_gap_etc_transposed_column_extend_before_witness_row_choice_left + S (p * S etc_row_index_transposed_column_extend_before) = q * S eri_column_etc_transposed_column_extend_before_witness_row) /\ ~(exists eri_gap_etc_transposed_column_extend_before_witness_row_choice_right. eri_gap_etc_transposed_column_extend_before_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_extend_before_witness_row) = p * S etc_row_index_transposed_column_extend_before))) \/ (eri_bit_etc_transposed_column_extend_before_witness_row = 1 /\ ((exists eri_gap_etc_transposed_column_extend_before_witness_row_choice_right. eri_gap_etc_transposed_column_extend_before_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_extend_before_witness_row) = p * S etc_row_index_transposed_column_extend_before) /\ ~(exists eri_gap_etc_transposed_column_extend_before_witness_row_choice_left. eri_gap_etc_transposed_column_extend_before_witness_row_choice_left + S (p * S etc_row_index_transposed_column_extend_before) = q * S eri_column_etc_transposed_column_extend_before_witness_row)))))))) /\ (((exists ff_u_etc_transposed_column_extend_before_witness_count_relation_sum ff_v_etc_transposed_column_extend_before_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_extend_before_witness_count_relation_sum_start. ff_h_etc_transposed_column_extend_before_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_extend_before_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_before_witness_count_relation_sum_start. ff_u_etc_transposed_column_extend_before_witness_count_relation_sum = ff_q_etc_transposed_column_extend_before_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_extend_before_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_extend_before_witness_count_relation_sum_terminal. ff_h_etc_transposed_column_extend_before_witness_count_relation_sum_terminal + S (etc_count_transposed_column_extend_before_witness) = S ((S (h)) * ff_v_etc_transposed_column_extend_before_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_before_witness_count_relation_sum_terminal. ff_u_etc_transposed_column_extend_before_witness_count_relation_sum = ff_q_etc_transposed_column_extend_before_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_extend_before_witness_count_relation_sum) + (etc_count_transposed_column_extend_before_witness))) /\ forall ff_i_etc_transposed_column_extend_before_witness_count_relation_sum. (exists ff_lt_etc_transposed_column_extend_before_witness_count_relation_sum_bound. ff_lt_etc_transposed_column_extend_before_witness_count_relation_sum_bound + S ff_i_etc_transposed_column_extend_before_witness_count_relation_sum = h) -> exists ff_a_etc_transposed_column_extend_before_witness_count_relation_sum ff_r_etc_transposed_column_extend_before_witness_count_relation_sum ff_s_etc_transposed_column_extend_before_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_extend_before_witness_count_relation_sum_summand. ff_h_etc_transposed_column_extend_before_witness_count_relation_sum_summand + S (ff_a_etc_transposed_column_extend_before_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_extend_before_witness_count_relation_sum)) * etc_row_scale_transposed_column_extend_before_witness)) /\ exists ff_q_etc_transposed_column_extend_before_witness_count_relation_sum_summand. etc_row_code_transposed_column_extend_before_witness = ff_q_etc_transposed_column_extend_before_witness_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_extend_before_witness_count_relation_sum)) * etc_row_scale_transposed_column_extend_before_witness) + (ff_a_etc_transposed_column_extend_before_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_extend_before_witness_count_relation_sum_partial. ff_h_etc_transposed_column_extend_before_witness_count_relation_sum_partial + S (ff_r_etc_transposed_column_extend_before_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_extend_before_witness_count_relation_sum)) * ff_v_etc_transposed_column_extend_before_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_before_witness_count_relation_sum_partial. ff_u_etc_transposed_column_extend_before_witness_count_relation_sum = ff_q_etc_transposed_column_extend_before_witness_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_extend_before_witness_count_relation_sum)) * ff_v_etc_transposed_column_extend_before_witness_count_relation_sum) + (ff_r_etc_transposed_column_extend_before_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_extend_before_witness_count_relation_sum_successor. ff_h_etc_transposed_column_extend_before_witness_count_relation_sum_successor + S (ff_s_etc_transposed_column_extend_before_witness_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_extend_before_witness_count_relation_sum)) * ff_v_etc_transposed_column_extend_before_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_before_witness_count_relation_sum_successor. ff_u_etc_transposed_column_extend_before_witness_count_relation_sum = ff_q_etc_transposed_column_extend_before_witness_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_extend_before_witness_count_relation_sum)) * ff_v_etc_transposed_column_extend_before_witness_count_relation_sum) + (ff_s_etc_transposed_column_extend_before_witness_count_relation_sum))) /\ ff_s_etc_transposed_column_extend_before_witness_count_relation_sum = ff_r_etc_transposed_column_extend_before_witness_count_relation_sum + ff_a_etc_transposed_column_extend_before_witness_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_extend_before_witness_count_relation_bits. (exists ff_lt_etc_transposed_column_extend_before_witness_count_relation_bits_bound. ff_lt_etc_transposed_column_extend_before_witness_count_relation_bits_bound + S ff_i_etc_transposed_column_extend_before_witness_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_extend_before_witness_count_relation_bits. ((((exists ff_h_etc_transposed_column_extend_before_witness_count_relation_bits_decoded. ff_h_etc_transposed_column_extend_before_witness_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_extend_before_witness_count_relation_bits) = S ((S (ff_i_etc_transposed_column_extend_before_witness_count_relation_bits)) * etc_row_scale_transposed_column_extend_before_witness)) /\ exists ff_q_etc_transposed_column_extend_before_witness_count_relation_bits_decoded. etc_row_code_transposed_column_extend_before_witness = ff_q_etc_transposed_column_extend_before_witness_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_extend_before_witness_count_relation_bits)) * etc_row_scale_transposed_column_extend_before_witness) + (ff_bit_etc_transposed_column_extend_before_witness_count_relation_bits))) /\ (ff_bit_etc_transposed_column_extend_before_witness_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_extend_before_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_extend_before_witness_inner_entry. ff_h_etc_transposed_column_extend_before_witness_inner_entry + S (etc_bit_transposed_column_extend_before) = S ((S (i)) * etc_row_scale_transposed_column_extend_before_witness)) /\ exists ff_q_etc_transposed_column_extend_before_witness_inner_entry. etc_row_code_transposed_column_extend_before_witness = ff_q_etc_transposed_column_extend_before_witness_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_extend_before_witness) + (etc_bit_transposed_column_extend_before))))))) -> (exists d. (exists etc_count_transposed_column_extend_last etc_row_code_transposed_column_extend_last etc_row_scale_transposed_column_extend_last. ((((((exists ff_h_etc_transposed_column_extend_last_outer_entry. ff_h_etc_transposed_column_extend_last_outer_entry + S (etc_count_transposed_column_extend_last) = S ((S (l)) * bc)) /\ exists ff_q_etc_transposed_column_extend_last_outer_entry. bb = ff_q_etc_transposed_column_extend_last_outer_entry * S ((S (l)) * bc) + (etc_count_transposed_column_extend_last))) /\ (forall eri_column_etc_transposed_column_extend_last_row. (exists eri_gap_etc_transposed_column_extend_last_row_bound. eri_gap_etc_transposed_column_extend_last_row_bound + S (eri_column_etc_transposed_column_extend_last_row) = h) -> exists eri_bit_etc_transposed_column_extend_last_row. ((((exists ff_h_eri_etc_transposed_column_extend_last_row_decoded. ff_h_eri_etc_transposed_column_extend_last_row_decoded + S (eri_bit_etc_transposed_column_extend_last_row) = S ((S (eri_column_etc_transposed_column_extend_last_row)) * etc_row_scale_transposed_column_extend_last)) /\ exists ff_q_eri_etc_transposed_column_extend_last_row_decoded. etc_row_code_transposed_column_extend_last = ff_q_eri_etc_transposed_column_extend_last_row_decoded * S ((S (eri_column_etc_transposed_column_extend_last_row)) * etc_row_scale_transposed_column_extend_last) + (eri_bit_etc_transposed_column_extend_last_row))) /\ (((eri_bit_etc_transposed_column_extend_last_row = 0 /\ ((exists eri_gap_etc_transposed_column_extend_last_row_choice_left. eri_gap_etc_transposed_column_extend_last_row_choice_left + S (p * S l) = q * S eri_column_etc_transposed_column_extend_last_row) /\ ~(exists eri_gap_etc_transposed_column_extend_last_row_choice_right. eri_gap_etc_transposed_column_extend_last_row_choice_right + S (q * S eri_column_etc_transposed_column_extend_last_row) = p * S l))) \/ (eri_bit_etc_transposed_column_extend_last_row = 1 /\ ((exists eri_gap_etc_transposed_column_extend_last_row_choice_right. eri_gap_etc_transposed_column_extend_last_row_choice_right + S (q * S eri_column_etc_transposed_column_extend_last_row) = p * S l) /\ ~(exists eri_gap_etc_transposed_column_extend_last_row_choice_left. eri_gap_etc_transposed_column_extend_last_row_choice_left + S (p * S l) = q * S eri_column_etc_transposed_column_extend_last_row)))))))) /\ (((exists ff_u_etc_transposed_column_extend_last_count_relation_sum ff_v_etc_transposed_column_extend_last_count_relation_sum. ((((exists ff_h_etc_transposed_column_extend_last_count_relation_sum_start. ff_h_etc_transposed_column_extend_last_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_extend_last_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_last_count_relation_sum_start. ff_u_etc_transposed_column_extend_last_count_relation_sum = ff_q_etc_transposed_column_extend_last_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_extend_last_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_extend_last_count_relation_sum_terminal. ff_h_etc_transposed_column_extend_last_count_relation_sum_terminal + S (etc_count_transposed_column_extend_last) = S ((S (h)) * ff_v_etc_transposed_column_extend_last_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_last_count_relation_sum_terminal. ff_u_etc_transposed_column_extend_last_count_relation_sum = ff_q_etc_transposed_column_extend_last_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_extend_last_count_relation_sum) + (etc_count_transposed_column_extend_last))) /\ forall ff_i_etc_transposed_column_extend_last_count_relation_sum. (exists ff_lt_etc_transposed_column_extend_last_count_relation_sum_bound. ff_lt_etc_transposed_column_extend_last_count_relation_sum_bound + S ff_i_etc_transposed_column_extend_last_count_relation_sum = h) -> exists ff_a_etc_transposed_column_extend_last_count_relation_sum ff_r_etc_transposed_column_extend_last_count_relation_sum ff_s_etc_transposed_column_extend_last_count_relation_sum. ((((exists ff_h_etc_transposed_column_extend_last_count_relation_sum_summand. ff_h_etc_transposed_column_extend_last_count_relation_sum_summand + S (ff_a_etc_transposed_column_extend_last_count_relation_sum) = S ((S (ff_i_etc_transposed_column_extend_last_count_relation_sum)) * etc_row_scale_transposed_column_extend_last)) /\ exists ff_q_etc_transposed_column_extend_last_count_relation_sum_summand. etc_row_code_transposed_column_extend_last = ff_q_etc_transposed_column_extend_last_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_extend_last_count_relation_sum)) * etc_row_scale_transposed_column_extend_last) + (ff_a_etc_transposed_column_extend_last_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_extend_last_count_relation_sum_partial. ff_h_etc_transposed_column_extend_last_count_relation_sum_partial + S (ff_r_etc_transposed_column_extend_last_count_relation_sum) = S ((S (ff_i_etc_transposed_column_extend_last_count_relation_sum)) * ff_v_etc_transposed_column_extend_last_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_last_count_relation_sum_partial. ff_u_etc_transposed_column_extend_last_count_relation_sum = ff_q_etc_transposed_column_extend_last_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_extend_last_count_relation_sum)) * ff_v_etc_transposed_column_extend_last_count_relation_sum) + (ff_r_etc_transposed_column_extend_last_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_extend_last_count_relation_sum_successor. ff_h_etc_transposed_column_extend_last_count_relation_sum_successor + S (ff_s_etc_transposed_column_extend_last_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_extend_last_count_relation_sum)) * ff_v_etc_transposed_column_extend_last_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_last_count_relation_sum_successor. ff_u_etc_transposed_column_extend_last_count_relation_sum = ff_q_etc_transposed_column_extend_last_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_extend_last_count_relation_sum)) * ff_v_etc_transposed_column_extend_last_count_relation_sum) + (ff_s_etc_transposed_column_extend_last_count_relation_sum))) /\ ff_s_etc_transposed_column_extend_last_count_relation_sum = ff_r_etc_transposed_column_extend_last_count_relation_sum + ff_a_etc_transposed_column_extend_last_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_extend_last_count_relation_bits. (exists ff_lt_etc_transposed_column_extend_last_count_relation_bits_bound. ff_lt_etc_transposed_column_extend_last_count_relation_bits_bound + S ff_i_etc_transposed_column_extend_last_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_extend_last_count_relation_bits. ((((exists ff_h_etc_transposed_column_extend_last_count_relation_bits_decoded. ff_h_etc_transposed_column_extend_last_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_extend_last_count_relation_bits) = S ((S (ff_i_etc_transposed_column_extend_last_count_relation_bits)) * etc_row_scale_transposed_column_extend_last)) /\ exists ff_q_etc_transposed_column_extend_last_count_relation_bits_decoded. etc_row_code_transposed_column_extend_last = ff_q_etc_transposed_column_extend_last_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_extend_last_count_relation_bits)) * etc_row_scale_transposed_column_extend_last) + (ff_bit_etc_transposed_column_extend_last_count_relation_bits))) /\ (ff_bit_etc_transposed_column_extend_last_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_extend_last_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_extend_last_inner_entry. ff_h_etc_transposed_column_extend_last_inner_entry + S (d) = S ((S (i)) * etc_row_scale_transposed_column_extend_last)) /\ exists ff_q_etc_transposed_column_extend_last_inner_entry. etc_row_code_transposed_column_extend_last = ff_q_etc_transposed_column_extend_last_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_extend_last) + (d)))))) -> exists u v. (forall etc_row_index_transposed_column_extend_after. (exists edt_lt_gap_transposed_column_extend_after_bound. edt_lt_gap_transposed_column_extend_after_bound + S (etc_row_index_transposed_column_extend_after) = S l) -> exists etc_bit_transposed_column_extend_after. ((((exists ff_h_etc_transposed_column_extend_after_decoded. ff_h_etc_transposed_column_extend_after_decoded + S (etc_bit_transposed_column_extend_after) = S ((S (etc_row_index_transposed_column_extend_after)) * v)) /\ exists ff_q_etc_transposed_column_extend_after_decoded. u = ff_q_etc_transposed_column_extend_after_decoded * S ((S (etc_row_index_transposed_column_extend_after)) * v) + (etc_bit_transposed_column_extend_after))) /\ (exists etc_count_transposed_column_extend_after_witness etc_row_code_transposed_column_extend_after_witness etc_row_scale_transposed_column_extend_after_witness. ((((((exists ff_h_etc_transposed_column_extend_after_witness_outer_entry. ff_h_etc_transposed_column_extend_after_witness_outer_entry + S (etc_count_transposed_column_extend_after_witness) = S ((S (etc_row_index_transposed_column_extend_after)) * bc)) /\ exists ff_q_etc_transposed_column_extend_after_witness_outer_entry. bb = ff_q_etc_transposed_column_extend_after_witness_outer_entry * S ((S (etc_row_index_transposed_column_extend_after)) * bc) + (etc_count_transposed_column_extend_after_witness))) /\ (forall eri_column_etc_transposed_column_extend_after_witness_row. (exists eri_gap_etc_transposed_column_extend_after_witness_row_bound. eri_gap_etc_transposed_column_extend_after_witness_row_bound + S (eri_column_etc_transposed_column_extend_after_witness_row) = h) -> exists eri_bit_etc_transposed_column_extend_after_witness_row. ((((exists ff_h_eri_etc_transposed_column_extend_after_witness_row_decoded. ff_h_eri_etc_transposed_column_extend_after_witness_row_decoded + S (eri_bit_etc_transposed_column_extend_after_witness_row) = S ((S (eri_column_etc_transposed_column_extend_after_witness_row)) * etc_row_scale_transposed_column_extend_after_witness)) /\ exists ff_q_eri_etc_transposed_column_extend_after_witness_row_decoded. etc_row_code_transposed_column_extend_after_witness = ff_q_eri_etc_transposed_column_extend_after_witness_row_decoded * S ((S (eri_column_etc_transposed_column_extend_after_witness_row)) * etc_row_scale_transposed_column_extend_after_witness) + (eri_bit_etc_transposed_column_extend_after_witness_row))) /\ (((eri_bit_etc_transposed_column_extend_after_witness_row = 0 /\ ((exists eri_gap_etc_transposed_column_extend_after_witness_row_choice_left. eri_gap_etc_transposed_column_extend_after_witness_row_choice_left + S (p * S etc_row_index_transposed_column_extend_after) = q * S eri_column_etc_transposed_column_extend_after_witness_row) /\ ~(exists eri_gap_etc_transposed_column_extend_after_witness_row_choice_right. eri_gap_etc_transposed_column_extend_after_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_extend_after_witness_row) = p * S etc_row_index_transposed_column_extend_after))) \/ (eri_bit_etc_transposed_column_extend_after_witness_row = 1 /\ ((exists eri_gap_etc_transposed_column_extend_after_witness_row_choice_right. eri_gap_etc_transposed_column_extend_after_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_extend_after_witness_row) = p * S etc_row_index_transposed_column_extend_after) /\ ~(exists eri_gap_etc_transposed_column_extend_after_witness_row_choice_left. eri_gap_etc_transposed_column_extend_after_witness_row_choice_left + S (p * S etc_row_index_transposed_column_extend_after) = q * S eri_column_etc_transposed_column_extend_after_witness_row)))))))) /\ (((exists ff_u_etc_transposed_column_extend_after_witness_count_relation_sum ff_v_etc_transposed_column_extend_after_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_extend_after_witness_count_relation_sum_start. ff_h_etc_transposed_column_extend_after_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_extend_after_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_after_witness_count_relation_sum_start. ff_u_etc_transposed_column_extend_after_witness_count_relation_sum = ff_q_etc_transposed_column_extend_after_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_extend_after_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_extend_after_witness_count_relation_sum_terminal. ff_h_etc_transposed_column_extend_after_witness_count_relation_sum_terminal + S (etc_count_transposed_column_extend_after_witness) = S ((S (h)) * ff_v_etc_transposed_column_extend_after_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_after_witness_count_relation_sum_terminal. ff_u_etc_transposed_column_extend_after_witness_count_relation_sum = ff_q_etc_transposed_column_extend_after_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_extend_after_witness_count_relation_sum) + (etc_count_transposed_column_extend_after_witness))) /\ forall ff_i_etc_transposed_column_extend_after_witness_count_relation_sum. (exists ff_lt_etc_transposed_column_extend_after_witness_count_relation_sum_bound. ff_lt_etc_transposed_column_extend_after_witness_count_relation_sum_bound + S ff_i_etc_transposed_column_extend_after_witness_count_relation_sum = h) -> exists ff_a_etc_transposed_column_extend_after_witness_count_relation_sum ff_r_etc_transposed_column_extend_after_witness_count_relation_sum ff_s_etc_transposed_column_extend_after_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_extend_after_witness_count_relation_sum_summand. ff_h_etc_transposed_column_extend_after_witness_count_relation_sum_summand + S (ff_a_etc_transposed_column_extend_after_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_extend_after_witness_count_relation_sum)) * etc_row_scale_transposed_column_extend_after_witness)) /\ exists ff_q_etc_transposed_column_extend_after_witness_count_relation_sum_summand. etc_row_code_transposed_column_extend_after_witness = ff_q_etc_transposed_column_extend_after_witness_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_extend_after_witness_count_relation_sum)) * etc_row_scale_transposed_column_extend_after_witness) + (ff_a_etc_transposed_column_extend_after_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_extend_after_witness_count_relation_sum_partial. ff_h_etc_transposed_column_extend_after_witness_count_relation_sum_partial + S (ff_r_etc_transposed_column_extend_after_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_extend_after_witness_count_relation_sum)) * ff_v_etc_transposed_column_extend_after_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_after_witness_count_relation_sum_partial. ff_u_etc_transposed_column_extend_after_witness_count_relation_sum = ff_q_etc_transposed_column_extend_after_witness_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_extend_after_witness_count_relation_sum)) * ff_v_etc_transposed_column_extend_after_witness_count_relation_sum) + (ff_r_etc_transposed_column_extend_after_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_extend_after_witness_count_relation_sum_successor. ff_h_etc_transposed_column_extend_after_witness_count_relation_sum_successor + S (ff_s_etc_transposed_column_extend_after_witness_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_extend_after_witness_count_relation_sum)) * ff_v_etc_transposed_column_extend_after_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_after_witness_count_relation_sum_successor. ff_u_etc_transposed_column_extend_after_witness_count_relation_sum = ff_q_etc_transposed_column_extend_after_witness_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_extend_after_witness_count_relation_sum)) * ff_v_etc_transposed_column_extend_after_witness_count_relation_sum) + (ff_s_etc_transposed_column_extend_after_witness_count_relation_sum))) /\ ff_s_etc_transposed_column_extend_after_witness_count_relation_sum = ff_r_etc_transposed_column_extend_after_witness_count_relation_sum + ff_a_etc_transposed_column_extend_after_witness_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_extend_after_witness_count_relation_bits. (exists ff_lt_etc_transposed_column_extend_after_witness_count_relation_bits_bound. ff_lt_etc_transposed_column_extend_after_witness_count_relation_bits_bound + S ff_i_etc_transposed_column_extend_after_witness_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_extend_after_witness_count_relation_bits. ((((exists ff_h_etc_transposed_column_extend_after_witness_count_relation_bits_decoded. ff_h_etc_transposed_column_extend_after_witness_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_extend_after_witness_count_relation_bits) = S ((S (ff_i_etc_transposed_column_extend_after_witness_count_relation_bits)) * etc_row_scale_transposed_column_extend_after_witness)) /\ exists ff_q_etc_transposed_column_extend_after_witness_count_relation_bits_decoded. etc_row_code_transposed_column_extend_after_witness = ff_q_etc_transposed_column_extend_after_witness_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_extend_after_witness_count_relation_bits)) * etc_row_scale_transposed_column_extend_after_witness) + (ff_bit_etc_transposed_column_extend_after_witness_count_relation_bits))) /\ (ff_bit_etc_transposed_column_extend_after_witness_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_extend_after_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_extend_after_witness_inner_entry. ff_h_etc_transposed_column_extend_after_witness_inner_entry + S (etc_bit_transposed_column_extend_after) = S ((S (i)) * etc_row_scale_transposed_column_extend_after_witness)) /\ exists ff_q_etc_transposed_column_extend_after_witness_inner_entry. etc_row_code_transposed_column_extend_after_witness = ff_q_etc_transposed_column_extend_after_witness_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_extend_after_witness) + (etc_bit_transposed_column_extend_after)))))))

Structural proof guide

Generated structural guide

Append one provenance-carrying swapped-row bit to a transposed column.

Use the direct prerequisites beta_prefix_extend, finite_lt_succ_eq_or_lt as previously established PA formulas.

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

Referenced ingredients

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Proof neighborhood

Direct dependencies

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Direct dependents

PA00E9 eisenstein_transposed_column_prefix_exists

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

55 script commands · 20 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)
beta prefix extendfinite lt succ eq or lt

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 bb
  5. L5
    intro bc
  6. L6
    intro i
  7. L7
    intro z
  8. L8
    intro e
  9. L9
    intro l
  10. L10
    intro hprefix
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hlast
03Separate the logical casesL12–12

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

  1. L12
    cases hlast
04Use earlier factsL13–16

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

  1. L13
    specialize beta_prefix_extend l
  2. L14
    specialize beta_prefix_extend z
  3. L15
    specialize beta_prefix_extend e
  4. L16
    specialize beta_prefix_extend x
05Separate the logical casesL17–19

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

  1. L17
    cases beta_prefix_extend
  2. L18
    cases beta_prefix_extend_witness
  3. L19
    cases beta_prefix_extend_witness_witness
06Construct an explicit witnessL20–21

Supply the displayed value, then prove that it has the required property.

  1. L20
    exists x1
  2. L21
    exists x2
07Fix variables and assumptionsL22–23

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

  1. L22
    intro j
  2. L23
    intro hj
08Establish hsplitL24–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L24
    have hsplit : j = l \/ exists gap. gap + S j = l
  2. L25
    specialize finite_lt_succ_eq_or_lt l
  3. L26
    specialize finite_lt_succ_eq_or_lt j
  4. L27
    apply finite_lt_succ_eq_or_lt
  5. L28
    exact hj
09Separate the logical casesL29–29

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

  1. L29
    cases hsplit
10Construct an explicit witnessL30–30

Supply the displayed value, then prove that it has the required property.

  1. L30
    exists x
11Separate the logical casesL31–31

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

  1. L31
    split
12Calculate and transport equalitiesL32–33

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

  1. L32
    rewrite hsplit_left
  2. L33
    rewrite hsplit_left
13Use earlier factsL34–34

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

  1. L34
    exact beta_prefix_extend_witness_witness_left
14Calculate and transport equalitiesL35–40

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

  1. L35
    rewrite hsplit_left
  2. L36
    rewrite hsplit_left
  3. L37
    rewrite hsplit_left
  4. L38
    rewrite hsplit_left
  5. L39
    rewrite hsplit_left
  6. L40
    rewrite hsplit_left
15Use earlier factsL41–41

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

  1. L41
    exact hlast_witness
16Establish holdL42–45

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

  1. L42
    have hold : ∃ oldbit. BetaAt(z,e,j,oldbit) ∧ (∃ x. ∃ y. ∃ n. BetaAt(bb,bc,j,x) ∧ (∀ m. Lt(m,h) → ∃ k. BetaAt(y,n,m,k) ∧ (k = 0 ∧ (Lt(p · S j,q · S m) ∧ ¬Lt(q · S m,p · S j)) ∨ k = 1 ∧ (Lt(q · S m,p · S j) ∧ ¬Lt(p · S j,q · S m)))) ∧ BitCount(y,n,h,x) ∧ BetaAt(y,n,i,oldbit))Definitions: LtBetaAtBitCount
  2. L43
    specialize hprefix j
  3. L44
    apply hprefix
  4. L45
    exact hsplit_right
17Separate the logical casesL46–47

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

  1. L46
    cases hold
  2. L47
    cases hold_witness
18Construct an explicit witnessL48–48

Supply the displayed value, then prove that it has the required property.

  1. L48
    exists x3
19Separate the logical casesL49–49

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

  1. L49
    split
20Use earlier factsL50–55

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

  1. L50
    specialize beta_prefix_extend_witness_witness_right j
  2. L51
    specialize beta_prefix_extend_witness_witness_right x3
  3. L52
    apply beta_prefix_extend_witness_witness_right
  4. L53
    exact hsplit_right
  5. L54
    exact hold_witness_left
  6. L55
    exact hold_witness_right

Library-wide reading audit

Original exact command ledger · 55 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro i
  7. 0007intro z
  8. 0008intro e
  9. 0009intro l
  10. 0010intro hprefix
  11. 0011intro hlast
  12. 0012cases hlast
  13. 0013specialize beta_prefix_extend l
  14. 0014specialize beta_prefix_extend z
  15. 0015specialize beta_prefix_extend e
  16. 0016specialize beta_prefix_extend x
  17. 0017cases beta_prefix_extend
  18. 0018cases beta_prefix_extend_witness
  19. 0019cases beta_prefix_extend_witness_witness
  20. 0020exists x1
  21. 0021exists x2
  22. 0022intro j
  23. 0023intro hj
  24. 0024have hsplit : j = l \/ exists gap. gap + S j = l
  25. 0025specialize finite_lt_succ_eq_or_lt l
  26. 0026specialize finite_lt_succ_eq_or_lt j
  27. 0027apply finite_lt_succ_eq_or_lt
  28. 0028exact hj
  29. 0029cases hsplit
  30. 0030exists x
  31. 0031split
  32. 0032rewrite hsplit_left
  33. 0033rewrite hsplit_left
  34. 0034exact beta_prefix_extend_witness_witness_left
  35. 0035rewrite hsplit_left
  36. 0036rewrite hsplit_left
  37. 0037rewrite hsplit_left
  38. 0038rewrite hsplit_left
  39. 0039rewrite hsplit_left
  40. 0040rewrite hsplit_left
  41. 0041exact hlast_witness
  42. 0042have hold : exists oldbit. ((((exists ff_h_transposed_column_extend_old_entry. ff_h_transposed_column_extend_old_entry + S (oldbit) = S ((S (j)) * e)) /\ exists ff_q_transposed_column_extend_old_entry. z = ff_q_transposed_column_extend_old_entry * S ((S (j)) * e) + (oldbit))) /\ (exists etc_count_transposed_column_extend_old_witness etc_row_code_transposed_column_extend_old_witness etc_row_scale_transposed_column_extend_old_witness. ((((((exists ff_h_etc_transposed_column_extend_old_witness_outer_entry. ff_h_etc_transposed_column_extend_old_witness_outer_entry + S (etc_count_transposed_column_extend_old_witness) = S ((S (j)) * bc)) /\ exists ff_q_etc_transposed_column_extend_old_witness_outer_entry. bb = ff_q_etc_transposed_column_extend_old_witness_outer_entry * S ((S (j)) * bc) + (etc_count_transposed_column_extend_old_witness))) /\ (forall eri_column_etc_transposed_column_extend_old_witness_row. (exists eri_gap_etc_transposed_column_extend_old_witness_row_bound. eri_gap_etc_transposed_column_extend_old_witness_row_bound + S (eri_column_etc_transposed_column_extend_old_witness_row) = h) -> exists eri_bit_etc_transposed_column_extend_old_witness_row. ((((exists ff_h_eri_etc_transposed_column_extend_old_witness_row_decoded. ff_h_eri_etc_transposed_column_extend_old_witness_row_decoded + S (eri_bit_etc_transposed_column_extend_old_witness_row) = S ((S (eri_column_etc_transposed_column_extend_old_witness_row)) * etc_row_scale_transposed_column_extend_old_witness)) /\ exists ff_q_eri_etc_transposed_column_extend_old_witness_row_decoded. etc_row_code_transposed_column_extend_old_witness = ff_q_eri_etc_transposed_column_extend_old_witness_row_decoded * S ((S (eri_column_etc_transposed_column_extend_old_witness_row)) * etc_row_scale_transposed_column_extend_old_witness) + (eri_bit_etc_transposed_column_extend_old_witness_row))) /\ (((eri_bit_etc_transposed_column_extend_old_witness_row = 0 /\ ((exists eri_gap_etc_transposed_column_extend_old_witness_row_choice_left. eri_gap_etc_transposed_column_extend_old_witness_row_choice_left + S (p * S j) = q * S eri_column_etc_transposed_column_extend_old_witness_row) /\ ~(exists eri_gap_etc_transposed_column_extend_old_witness_row_choice_right. eri_gap_etc_transposed_column_extend_old_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_extend_old_witness_row) = p * S j))) \/ (eri_bit_etc_transposed_column_extend_old_witness_row = 1 /\ ((exists eri_gap_etc_transposed_column_extend_old_witness_row_choice_right. eri_gap_etc_transposed_column_extend_old_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_extend_old_witness_row) = p * S j) /\ ~(exists eri_gap_etc_transposed_column_extend_old_witness_row_choice_left. eri_gap_etc_transposed_column_extend_old_witness_row_choice_left + S (p * S j) = q * S eri_column_etc_transposed_column_extend_old_witness_row)))))))) /\ (((exists ff_u_etc_transposed_column_extend_old_witness_count_relation_sum ff_v_etc_transposed_column_extend_old_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_extend_old_witness_count_relation_sum_start. ff_h_etc_transposed_column_extend_old_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_extend_old_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_old_witness_count_relation_sum_start. ff_u_etc_transposed_column_extend_old_witness_count_relation_sum = ff_q_etc_transposed_column_extend_old_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_extend_old_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_extend_old_witness_count_relation_sum_terminal. ff_h_etc_transposed_column_extend_old_witness_count_relation_sum_terminal + S (etc_count_transposed_column_extend_old_witness) = S ((S (h)) * ff_v_etc_transposed_column_extend_old_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_old_witness_count_relation_sum_terminal. ff_u_etc_transposed_column_extend_old_witness_count_relation_sum = ff_q_etc_transposed_column_extend_old_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_extend_old_witness_count_relation_sum) + (etc_count_transposed_column_extend_old_witness))) /\ forall ff_i_etc_transposed_column_extend_old_witness_count_relation_sum. (exists ff_lt_etc_transposed_column_extend_old_witness_count_relation_sum_bound. ff_lt_etc_transposed_column_extend_old_witness_count_relation_sum_bound + S ff_i_etc_transposed_column_extend_old_witness_count_relation_sum = h) -> exists ff_a_etc_transposed_column_extend_old_witness_count_relation_sum ff_r_etc_transposed_column_extend_old_witness_count_relation_sum ff_s_etc_transposed_column_extend_old_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_extend_old_witness_count_relation_sum_summand. ff_h_etc_transposed_column_extend_old_witness_count_relation_sum_summand + S (ff_a_etc_transposed_column_extend_old_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_extend_old_witness_count_relation_sum)) * etc_row_scale_transposed_column_extend_old_witness)) /\ exists ff_q_etc_transposed_column_extend_old_witness_count_relation_sum_summand. etc_row_code_transposed_column_extend_old_witness = ff_q_etc_transposed_column_extend_old_witness_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_extend_old_witness_count_relation_sum)) * etc_row_scale_transposed_column_extend_old_witness) + (ff_a_etc_transposed_column_extend_old_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_extend_old_witness_count_relation_sum_partial. ff_h_etc_transposed_column_extend_old_witness_count_relation_sum_partial + S (ff_r_etc_transposed_column_extend_old_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_extend_old_witness_count_relation_sum)) * ff_v_etc_transposed_column_extend_old_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_old_witness_count_relation_sum_partial. ff_u_etc_transposed_column_extend_old_witness_count_relation_sum = ff_q_etc_transposed_column_extend_old_witness_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_extend_old_witness_count_relation_sum)) * ff_v_etc_transposed_column_extend_old_witness_count_relation_sum) + (ff_r_etc_transposed_column_extend_old_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_extend_old_witness_count_relation_sum_successor. ff_h_etc_transposed_column_extend_old_witness_count_relation_sum_successor + S (ff_s_etc_transposed_column_extend_old_witness_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_extend_old_witness_count_relation_sum)) * ff_v_etc_transposed_column_extend_old_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_extend_old_witness_count_relation_sum_successor. ff_u_etc_transposed_column_extend_old_witness_count_relation_sum = ff_q_etc_transposed_column_extend_old_witness_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_extend_old_witness_count_relation_sum)) * ff_v_etc_transposed_column_extend_old_witness_count_relation_sum) + (ff_s_etc_transposed_column_extend_old_witness_count_relation_sum))) /\ ff_s_etc_transposed_column_extend_old_witness_count_relation_sum = ff_r_etc_transposed_column_extend_old_witness_count_relation_sum + ff_a_etc_transposed_column_extend_old_witness_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_extend_old_witness_count_relation_bits. (exists ff_lt_etc_transposed_column_extend_old_witness_count_relation_bits_bound. ff_lt_etc_transposed_column_extend_old_witness_count_relation_bits_bound + S ff_i_etc_transposed_column_extend_old_witness_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_extend_old_witness_count_relation_bits. ((((exists ff_h_etc_transposed_column_extend_old_witness_count_relation_bits_decoded. ff_h_etc_transposed_column_extend_old_witness_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_extend_old_witness_count_relation_bits) = S ((S (ff_i_etc_transposed_column_extend_old_witness_count_relation_bits)) * etc_row_scale_transposed_column_extend_old_witness)) /\ exists ff_q_etc_transposed_column_extend_old_witness_count_relation_bits_decoded. etc_row_code_transposed_column_extend_old_witness = ff_q_etc_transposed_column_extend_old_witness_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_extend_old_witness_count_relation_bits)) * etc_row_scale_transposed_column_extend_old_witness) + (ff_bit_etc_transposed_column_extend_old_witness_count_relation_bits))) /\ (ff_bit_etc_transposed_column_extend_old_witness_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_extend_old_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_extend_old_witness_inner_entry. ff_h_etc_transposed_column_extend_old_witness_inner_entry + S (oldbit) = S ((S (i)) * etc_row_scale_transposed_column_extend_old_witness)) /\ exists ff_q_etc_transposed_column_extend_old_witness_inner_entry. etc_row_code_transposed_column_extend_old_witness = ff_q_etc_transposed_column_extend_old_witness_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_extend_old_witness) + (oldbit))))))
  43. 0043specialize hprefix j
  44. 0044apply hprefix
  45. 0045exact hsplit_right
  46. 0046cases hold
  47. 0047cases hold_witness
  48. 0048exists x3
  49. 0049split
  50. 0050specialize beta_prefix_extend_witness_witness_right j
  51. 0051specialize beta_prefix_extend_witness_witness_right x3
  52. 0052apply beta_prefix_extend_witness_witness_right
  53. 0053exact hsplit_right
  54. 0054exact hold_witness_left
  55. 0055exact hold_witness_right