PA00DI · theorem

eisenstein_rectangle_row_count_prefix_extend

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

Append one semantic row count while preserving all earlier rows.

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

Statement with defined notation

∀ p. ∀ q. ∀ k. ∀ cb. ∀ cc. ∀ l. (∀ x. Lt(x,l) → ∃ y. BetaAt(cb,cc,x,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,k) → ∃ i. BetaAt(z,n,m,i) ∧ (i = 0 ∧ (Lt(q · S x,p · S m) ∧ ¬Lt(p · S m,q · S x)) ∨ i = 1 ∧ (Lt(p · S m,q · S x) ∧ ¬Lt(q · S x,p · S m)))) ∧ BitCount(z,n,k,y))) → (∃ x. ∃ y. ∃ z. (∀ n. Lt(n,k) → ∃ m. BetaAt(y,z,n,m) ∧ (m = 0 ∧ (Lt(q · S l,p · S n) ∧ ¬Lt(p · S n,q · S l)) ∨ m = 1 ∧ (Lt(p · S n,q · S l) ∧ ¬Lt(q · S l,p · S n)))) ∧ BitCount(y,z,k,x)) → ∃ x. ∃ y. ∀ z. Lt(z,S l) → ∃ n. BetaAt(x,y,z,n) ∧ (∃ m. ∃ i. (∀ j. Lt(j,k) → ∃ u. BetaAt(m,i,j,u) ∧ (u = 0 ∧ (Lt(q · S z,p · S j) ∧ ¬Lt(p · S j,q · S z)) ∨ u = 1 ∧ (Lt(p · S j,q · S z) ∧ ¬Lt(q · S z,p · S j)))) ∧ BitCount(m,i,k,n))

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

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0017 BitCount

25 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0017 BitCount

9 occurrences

Exact expanded native-PA statement
forall p q k cb cc l. (forall erc_row_rectangle_count_extend_before. (exists erc_lt_gap_rectangle_count_extend_before_bound. erc_lt_gap_rectangle_count_extend_before_bound + S (erc_row_rectangle_count_extend_before) = l) -> exists erc_count_rectangle_count_extend_before. ((((exists ff_h_erc_rectangle_count_extend_before_decoded. ff_h_erc_rectangle_count_extend_before_decoded + S (erc_count_rectangle_count_extend_before) = S ((S (erc_row_rectangle_count_extend_before)) * cc)) /\ exists ff_q_erc_rectangle_count_extend_before_decoded. cb = ff_q_erc_rectangle_count_extend_before_decoded * S ((S (erc_row_rectangle_count_extend_before)) * cc) + (erc_count_rectangle_count_extend_before))) /\ (exists erc_row_code_rectangle_count_extend_before_witness erc_row_scale_rectangle_count_extend_before_witness. ((forall eri_column_erc_rectangle_count_extend_before_witness_row. (exists eri_gap_erc_rectangle_count_extend_before_witness_row_bound. eri_gap_erc_rectangle_count_extend_before_witness_row_bound + S (eri_column_erc_rectangle_count_extend_before_witness_row) = k) -> exists eri_bit_erc_rectangle_count_extend_before_witness_row. ((((exists ff_h_eri_erc_rectangle_count_extend_before_witness_row_decoded. ff_h_eri_erc_rectangle_count_extend_before_witness_row_decoded + S (eri_bit_erc_rectangle_count_extend_before_witness_row) = S ((S (eri_column_erc_rectangle_count_extend_before_witness_row)) * erc_row_scale_rectangle_count_extend_before_witness)) /\ exists ff_q_eri_erc_rectangle_count_extend_before_witness_row_decoded. erc_row_code_rectangle_count_extend_before_witness = ff_q_eri_erc_rectangle_count_extend_before_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_extend_before_witness_row)) * erc_row_scale_rectangle_count_extend_before_witness) + (eri_bit_erc_rectangle_count_extend_before_witness_row))) /\ (((eri_bit_erc_rectangle_count_extend_before_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_extend_before_witness_row_choice_left. eri_gap_erc_rectangle_count_extend_before_witness_row_choice_left + S (q * S erc_row_rectangle_count_extend_before) = p * S eri_column_erc_rectangle_count_extend_before_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_extend_before_witness_row_choice_right. eri_gap_erc_rectangle_count_extend_before_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_before_witness_row) = q * S erc_row_rectangle_count_extend_before))) \/ (eri_bit_erc_rectangle_count_extend_before_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_extend_before_witness_row_choice_right. eri_gap_erc_rectangle_count_extend_before_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_before_witness_row) = q * S erc_row_rectangle_count_extend_before) /\ ~(exists eri_gap_erc_rectangle_count_extend_before_witness_row_choice_left. eri_gap_erc_rectangle_count_extend_before_witness_row_choice_left + S (q * S erc_row_rectangle_count_extend_before) = p * S eri_column_erc_rectangle_count_extend_before_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_extend_before_witness_count_sum ff_v_erc_rectangle_count_extend_before_witness_count_sum. ((((exists ff_h_erc_rectangle_count_extend_before_witness_count_sum_start. ff_h_erc_rectangle_count_extend_before_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_before_witness_count_sum_start. ff_u_erc_rectangle_count_extend_before_witness_count_sum = ff_q_erc_rectangle_count_extend_before_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_extend_before_witness_count_sum_terminal. ff_h_erc_rectangle_count_extend_before_witness_count_sum_terminal + S (erc_count_rectangle_count_extend_before) = S ((S (k)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_before_witness_count_sum_terminal. ff_u_erc_rectangle_count_extend_before_witness_count_sum = ff_q_erc_rectangle_count_extend_before_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum) + (erc_count_rectangle_count_extend_before))) /\ forall ff_i_erc_rectangle_count_extend_before_witness_count_sum. (exists ff_lt_erc_rectangle_count_extend_before_witness_count_sum_bound. ff_lt_erc_rectangle_count_extend_before_witness_count_sum_bound + S ff_i_erc_rectangle_count_extend_before_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_extend_before_witness_count_sum ff_r_erc_rectangle_count_extend_before_witness_count_sum ff_s_erc_rectangle_count_extend_before_witness_count_sum. ((((exists ff_h_erc_rectangle_count_extend_before_witness_count_sum_summand. ff_h_erc_rectangle_count_extend_before_witness_count_sum_summand + S (ff_a_erc_rectangle_count_extend_before_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_before_witness_count_sum)) * erc_row_scale_rectangle_count_extend_before_witness)) /\ exists ff_q_erc_rectangle_count_extend_before_witness_count_sum_summand. erc_row_code_rectangle_count_extend_before_witness = ff_q_erc_rectangle_count_extend_before_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_extend_before_witness_count_sum)) * erc_row_scale_rectangle_count_extend_before_witness) + (ff_a_erc_rectangle_count_extend_before_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_before_witness_count_sum_partial. ff_h_erc_rectangle_count_extend_before_witness_count_sum_partial + S (ff_r_erc_rectangle_count_extend_before_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_before_witness_count_sum)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_before_witness_count_sum_partial. ff_u_erc_rectangle_count_extend_before_witness_count_sum = ff_q_erc_rectangle_count_extend_before_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_extend_before_witness_count_sum)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum) + (ff_r_erc_rectangle_count_extend_before_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_before_witness_count_sum_successor. ff_h_erc_rectangle_count_extend_before_witness_count_sum_successor + S (ff_s_erc_rectangle_count_extend_before_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_extend_before_witness_count_sum)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_before_witness_count_sum_successor. ff_u_erc_rectangle_count_extend_before_witness_count_sum = ff_q_erc_rectangle_count_extend_before_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_extend_before_witness_count_sum)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum) + (ff_s_erc_rectangle_count_extend_before_witness_count_sum))) /\ ff_s_erc_rectangle_count_extend_before_witness_count_sum = ff_r_erc_rectangle_count_extend_before_witness_count_sum + ff_a_erc_rectangle_count_extend_before_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_extend_before_witness_count_bits. (exists ff_lt_erc_rectangle_count_extend_before_witness_count_bits_bound. ff_lt_erc_rectangle_count_extend_before_witness_count_bits_bound + S ff_i_erc_rectangle_count_extend_before_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_extend_before_witness_count_bits. ((((exists ff_h_erc_rectangle_count_extend_before_witness_count_bits_decoded. ff_h_erc_rectangle_count_extend_before_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_extend_before_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_extend_before_witness_count_bits)) * erc_row_scale_rectangle_count_extend_before_witness)) /\ exists ff_q_erc_rectangle_count_extend_before_witness_count_bits_decoded. erc_row_code_rectangle_count_extend_before_witness = ff_q_erc_rectangle_count_extend_before_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_extend_before_witness_count_bits)) * erc_row_scale_rectangle_count_extend_before_witness) + (ff_bit_erc_rectangle_count_extend_before_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_extend_before_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_extend_before_witness_count_bits = 1))))))))) -> (exists n. (exists erc_row_code_rectangle_count_extend_last erc_row_scale_rectangle_count_extend_last. ((forall eri_column_erc_rectangle_count_extend_last_row. (exists eri_gap_erc_rectangle_count_extend_last_row_bound. eri_gap_erc_rectangle_count_extend_last_row_bound + S (eri_column_erc_rectangle_count_extend_last_row) = k) -> exists eri_bit_erc_rectangle_count_extend_last_row. ((((exists ff_h_eri_erc_rectangle_count_extend_last_row_decoded. ff_h_eri_erc_rectangle_count_extend_last_row_decoded + S (eri_bit_erc_rectangle_count_extend_last_row) = S ((S (eri_column_erc_rectangle_count_extend_last_row)) * erc_row_scale_rectangle_count_extend_last)) /\ exists ff_q_eri_erc_rectangle_count_extend_last_row_decoded. erc_row_code_rectangle_count_extend_last = ff_q_eri_erc_rectangle_count_extend_last_row_decoded * S ((S (eri_column_erc_rectangle_count_extend_last_row)) * erc_row_scale_rectangle_count_extend_last) + (eri_bit_erc_rectangle_count_extend_last_row))) /\ (((eri_bit_erc_rectangle_count_extend_last_row = 0 /\ ((exists eri_gap_erc_rectangle_count_extend_last_row_choice_left. eri_gap_erc_rectangle_count_extend_last_row_choice_left + S (q * S l) = p * S eri_column_erc_rectangle_count_extend_last_row) /\ ~(exists eri_gap_erc_rectangle_count_extend_last_row_choice_right. eri_gap_erc_rectangle_count_extend_last_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_last_row) = q * S l))) \/ (eri_bit_erc_rectangle_count_extend_last_row = 1 /\ ((exists eri_gap_erc_rectangle_count_extend_last_row_choice_right. eri_gap_erc_rectangle_count_extend_last_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_last_row) = q * S l) /\ ~(exists eri_gap_erc_rectangle_count_extend_last_row_choice_left. eri_gap_erc_rectangle_count_extend_last_row_choice_left + S (q * S l) = p * S eri_column_erc_rectangle_count_extend_last_row))))))) /\ (((exists ff_u_erc_rectangle_count_extend_last_count_sum ff_v_erc_rectangle_count_extend_last_count_sum. ((((exists ff_h_erc_rectangle_count_extend_last_count_sum_start. ff_h_erc_rectangle_count_extend_last_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_extend_last_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_last_count_sum_start. ff_u_erc_rectangle_count_extend_last_count_sum = ff_q_erc_rectangle_count_extend_last_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_extend_last_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_extend_last_count_sum_terminal. ff_h_erc_rectangle_count_extend_last_count_sum_terminal + S (n) = S ((S (k)) * ff_v_erc_rectangle_count_extend_last_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_last_count_sum_terminal. ff_u_erc_rectangle_count_extend_last_count_sum = ff_q_erc_rectangle_count_extend_last_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_extend_last_count_sum) + (n))) /\ forall ff_i_erc_rectangle_count_extend_last_count_sum. (exists ff_lt_erc_rectangle_count_extend_last_count_sum_bound. ff_lt_erc_rectangle_count_extend_last_count_sum_bound + S ff_i_erc_rectangle_count_extend_last_count_sum = k) -> exists ff_a_erc_rectangle_count_extend_last_count_sum ff_r_erc_rectangle_count_extend_last_count_sum ff_s_erc_rectangle_count_extend_last_count_sum. ((((exists ff_h_erc_rectangle_count_extend_last_count_sum_summand. ff_h_erc_rectangle_count_extend_last_count_sum_summand + S (ff_a_erc_rectangle_count_extend_last_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_last_count_sum)) * erc_row_scale_rectangle_count_extend_last)) /\ exists ff_q_erc_rectangle_count_extend_last_count_sum_summand. erc_row_code_rectangle_count_extend_last = ff_q_erc_rectangle_count_extend_last_count_sum_summand * S ((S (ff_i_erc_rectangle_count_extend_last_count_sum)) * erc_row_scale_rectangle_count_extend_last) + (ff_a_erc_rectangle_count_extend_last_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_last_count_sum_partial. ff_h_erc_rectangle_count_extend_last_count_sum_partial + S (ff_r_erc_rectangle_count_extend_last_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_last_count_sum)) * ff_v_erc_rectangle_count_extend_last_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_last_count_sum_partial. ff_u_erc_rectangle_count_extend_last_count_sum = ff_q_erc_rectangle_count_extend_last_count_sum_partial * S ((S (ff_i_erc_rectangle_count_extend_last_count_sum)) * ff_v_erc_rectangle_count_extend_last_count_sum) + (ff_r_erc_rectangle_count_extend_last_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_last_count_sum_successor. ff_h_erc_rectangle_count_extend_last_count_sum_successor + S (ff_s_erc_rectangle_count_extend_last_count_sum) = S ((S (S ff_i_erc_rectangle_count_extend_last_count_sum)) * ff_v_erc_rectangle_count_extend_last_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_last_count_sum_successor. ff_u_erc_rectangle_count_extend_last_count_sum = ff_q_erc_rectangle_count_extend_last_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_extend_last_count_sum)) * ff_v_erc_rectangle_count_extend_last_count_sum) + (ff_s_erc_rectangle_count_extend_last_count_sum))) /\ ff_s_erc_rectangle_count_extend_last_count_sum = ff_r_erc_rectangle_count_extend_last_count_sum + ff_a_erc_rectangle_count_extend_last_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_extend_last_count_bits. (exists ff_lt_erc_rectangle_count_extend_last_count_bits_bound. ff_lt_erc_rectangle_count_extend_last_count_bits_bound + S ff_i_erc_rectangle_count_extend_last_count_bits = k) -> exists ff_bit_erc_rectangle_count_extend_last_count_bits. ((((exists ff_h_erc_rectangle_count_extend_last_count_bits_decoded. ff_h_erc_rectangle_count_extend_last_count_bits_decoded + S (ff_bit_erc_rectangle_count_extend_last_count_bits) = S ((S (ff_i_erc_rectangle_count_extend_last_count_bits)) * erc_row_scale_rectangle_count_extend_last)) /\ exists ff_q_erc_rectangle_count_extend_last_count_bits_decoded. erc_row_code_rectangle_count_extend_last = ff_q_erc_rectangle_count_extend_last_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_extend_last_count_bits)) * erc_row_scale_rectangle_count_extend_last) + (ff_bit_erc_rectangle_count_extend_last_count_bits))) /\ (ff_bit_erc_rectangle_count_extend_last_count_bits = 0 \/ ff_bit_erc_rectangle_count_extend_last_count_bits = 1)))))))) -> exists z d. (forall erc_row_rectangle_count_extend_after. (exists erc_lt_gap_rectangle_count_extend_after_bound. erc_lt_gap_rectangle_count_extend_after_bound + S (erc_row_rectangle_count_extend_after) = S l) -> exists erc_count_rectangle_count_extend_after. ((((exists ff_h_erc_rectangle_count_extend_after_decoded. ff_h_erc_rectangle_count_extend_after_decoded + S (erc_count_rectangle_count_extend_after) = S ((S (erc_row_rectangle_count_extend_after)) * d)) /\ exists ff_q_erc_rectangle_count_extend_after_decoded. z = ff_q_erc_rectangle_count_extend_after_decoded * S ((S (erc_row_rectangle_count_extend_after)) * d) + (erc_count_rectangle_count_extend_after))) /\ (exists erc_row_code_rectangle_count_extend_after_witness erc_row_scale_rectangle_count_extend_after_witness. ((forall eri_column_erc_rectangle_count_extend_after_witness_row. (exists eri_gap_erc_rectangle_count_extend_after_witness_row_bound. eri_gap_erc_rectangle_count_extend_after_witness_row_bound + S (eri_column_erc_rectangle_count_extend_after_witness_row) = k) -> exists eri_bit_erc_rectangle_count_extend_after_witness_row. ((((exists ff_h_eri_erc_rectangle_count_extend_after_witness_row_decoded. ff_h_eri_erc_rectangle_count_extend_after_witness_row_decoded + S (eri_bit_erc_rectangle_count_extend_after_witness_row) = S ((S (eri_column_erc_rectangle_count_extend_after_witness_row)) * erc_row_scale_rectangle_count_extend_after_witness)) /\ exists ff_q_eri_erc_rectangle_count_extend_after_witness_row_decoded. erc_row_code_rectangle_count_extend_after_witness = ff_q_eri_erc_rectangle_count_extend_after_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_extend_after_witness_row)) * erc_row_scale_rectangle_count_extend_after_witness) + (eri_bit_erc_rectangle_count_extend_after_witness_row))) /\ (((eri_bit_erc_rectangle_count_extend_after_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_extend_after_witness_row_choice_left. eri_gap_erc_rectangle_count_extend_after_witness_row_choice_left + S (q * S erc_row_rectangle_count_extend_after) = p * S eri_column_erc_rectangle_count_extend_after_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_extend_after_witness_row_choice_right. eri_gap_erc_rectangle_count_extend_after_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_after_witness_row) = q * S erc_row_rectangle_count_extend_after))) \/ (eri_bit_erc_rectangle_count_extend_after_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_extend_after_witness_row_choice_right. eri_gap_erc_rectangle_count_extend_after_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_after_witness_row) = q * S erc_row_rectangle_count_extend_after) /\ ~(exists eri_gap_erc_rectangle_count_extend_after_witness_row_choice_left. eri_gap_erc_rectangle_count_extend_after_witness_row_choice_left + S (q * S erc_row_rectangle_count_extend_after) = p * S eri_column_erc_rectangle_count_extend_after_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_extend_after_witness_count_sum ff_v_erc_rectangle_count_extend_after_witness_count_sum. ((((exists ff_h_erc_rectangle_count_extend_after_witness_count_sum_start. ff_h_erc_rectangle_count_extend_after_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_after_witness_count_sum_start. ff_u_erc_rectangle_count_extend_after_witness_count_sum = ff_q_erc_rectangle_count_extend_after_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_extend_after_witness_count_sum_terminal. ff_h_erc_rectangle_count_extend_after_witness_count_sum_terminal + S (erc_count_rectangle_count_extend_after) = S ((S (k)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_after_witness_count_sum_terminal. ff_u_erc_rectangle_count_extend_after_witness_count_sum = ff_q_erc_rectangle_count_extend_after_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum) + (erc_count_rectangle_count_extend_after))) /\ forall ff_i_erc_rectangle_count_extend_after_witness_count_sum. (exists ff_lt_erc_rectangle_count_extend_after_witness_count_sum_bound. ff_lt_erc_rectangle_count_extend_after_witness_count_sum_bound + S ff_i_erc_rectangle_count_extend_after_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_extend_after_witness_count_sum ff_r_erc_rectangle_count_extend_after_witness_count_sum ff_s_erc_rectangle_count_extend_after_witness_count_sum. ((((exists ff_h_erc_rectangle_count_extend_after_witness_count_sum_summand. ff_h_erc_rectangle_count_extend_after_witness_count_sum_summand + S (ff_a_erc_rectangle_count_extend_after_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_after_witness_count_sum)) * erc_row_scale_rectangle_count_extend_after_witness)) /\ exists ff_q_erc_rectangle_count_extend_after_witness_count_sum_summand. erc_row_code_rectangle_count_extend_after_witness = ff_q_erc_rectangle_count_extend_after_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_extend_after_witness_count_sum)) * erc_row_scale_rectangle_count_extend_after_witness) + (ff_a_erc_rectangle_count_extend_after_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_after_witness_count_sum_partial. ff_h_erc_rectangle_count_extend_after_witness_count_sum_partial + S (ff_r_erc_rectangle_count_extend_after_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_after_witness_count_sum)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_after_witness_count_sum_partial. ff_u_erc_rectangle_count_extend_after_witness_count_sum = ff_q_erc_rectangle_count_extend_after_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_extend_after_witness_count_sum)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum) + (ff_r_erc_rectangle_count_extend_after_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_after_witness_count_sum_successor. ff_h_erc_rectangle_count_extend_after_witness_count_sum_successor + S (ff_s_erc_rectangle_count_extend_after_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_extend_after_witness_count_sum)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_after_witness_count_sum_successor. ff_u_erc_rectangle_count_extend_after_witness_count_sum = ff_q_erc_rectangle_count_extend_after_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_extend_after_witness_count_sum)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum) + (ff_s_erc_rectangle_count_extend_after_witness_count_sum))) /\ ff_s_erc_rectangle_count_extend_after_witness_count_sum = ff_r_erc_rectangle_count_extend_after_witness_count_sum + ff_a_erc_rectangle_count_extend_after_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_extend_after_witness_count_bits. (exists ff_lt_erc_rectangle_count_extend_after_witness_count_bits_bound. ff_lt_erc_rectangle_count_extend_after_witness_count_bits_bound + S ff_i_erc_rectangle_count_extend_after_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_extend_after_witness_count_bits. ((((exists ff_h_erc_rectangle_count_extend_after_witness_count_bits_decoded. ff_h_erc_rectangle_count_extend_after_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_extend_after_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_extend_after_witness_count_bits)) * erc_row_scale_rectangle_count_extend_after_witness)) /\ exists ff_q_erc_rectangle_count_extend_after_witness_count_bits_decoded. erc_row_code_rectangle_count_extend_after_witness = ff_q_erc_rectangle_count_extend_after_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_extend_after_witness_count_bits)) * erc_row_scale_rectangle_count_extend_after_witness) + (ff_bit_erc_rectangle_count_extend_after_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_extend_after_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_extend_after_witness_count_bits = 1)))))))))

Proof neighborhood

Direct theorem prerequisites

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Direct theorem dependents

PA00DJ eisenstein_rectangle_row_count_prefix_exists

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

50 script commands · 19 reading checkpoints · 2 local claims

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

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

Named ingredients (2)
beta prefix extendfinite lt succ eq or lt
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro k
  4. L4
    intro cb
  5. L5
    intro cc
  6. L6
    intro l
  7. L7
    intro hprefix
  8. L8
    intro hchoice
02Separate the logical casesL9–9

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

  1. L9
    cases hchoice
03Use earlier factsL10–13

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

  1. L10
    specialize beta_prefix_extend l
  2. L11
    specialize beta_prefix_extend cb
  3. L12
    specialize beta_prefix_extend cc
  4. L13
    specialize beta_prefix_extend x
04Separate the logical casesL14–16

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

  1. L14
    cases beta_prefix_extend
  2. L15
    cases beta_prefix_extend_witness
  3. L16
    cases beta_prefix_extend_witness_witness
05Construct an explicit witnessL17–18

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

  1. L17
    exists x1
  2. L18
    exists x2
06Fix variables and assumptionsL19–20

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

  1. L19
    intro i
  2. L20
    intro hi
07Establish hsplitL21–25

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. L21
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L22
    specialize finite_lt_succ_eq_or_lt l
  3. L23
    specialize finite_lt_succ_eq_or_lt i
  4. L24
    apply finite_lt_succ_eq_or_lt
  5. L25
    exact hi
08Separate the logical casesL26–26

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

  1. L26
    cases hsplit
09Construct an explicit witnessL27–27

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

  1. L27
    exists x
10Separate the logical casesL28–28

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

  1. L28
    split
11Calculate and transport equalitiesL29–30

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

  1. L29
    rewrite hsplit_left
  2. L30
    rewrite hsplit_left
12Use earlier factsL31–31

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

  1. L31
    exact beta_prefix_extend_witness_witness_left
13Calculate and transport equalitiesL32–35

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
  3. L34
    rewrite hsplit_left
  4. L35
    rewrite hsplit_left
14Use earlier factsL36–36

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

  1. L36
    exact hchoice_witness
15Establish holdL37–40

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

  1. L37
    have hold : ∃ oldcount. BetaAt(cb,cc,i,oldcount) ∧ (∃ 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,oldcount))Definitions: BetaAt(cb,cc,i,oldcount)Lt(z,k)BetaAt(x,y,z,n)Lt(q · S i,p · S z)Lt(p · S z,q · S i)BitCount(x,y,k,oldcount)Original native command in the exact edition
  2. L38
    specialize hprefix i
  3. L39
    apply hprefix
  4. L40
    exact hsplit_right
16Separate the logical casesL41–42

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

  1. L41
    cases hold
  2. L42
    cases hold_witness
17Construct an explicit witnessL43–43

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

  1. L43
    exists x3
18Separate the logical casesL44–44

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

  1. L44
    split
19Use earlier factsL45–50

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

  1. L45
    specialize beta_prefix_extend_witness_witness_right i
  2. L46
    specialize beta_prefix_extend_witness_witness_right x3
  3. L47
    apply beta_prefix_extend_witness_witness_right
  4. L48
    exact hsplit_right
  5. L49
    exact hold_witness_left
  6. L50
    exact hold_witness_right

Library-wide reading audit

Original defined command ledger · 50 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro k
  4. 0004intro cb
  5. 0005intro cc
  6. 0006intro l
  7. 0007intro hprefix
  8. 0008intro hchoice
  9. 0009cases hchoice
  10. 0010specialize beta_prefix_extend l
  11. 0011specialize beta_prefix_extend cb
  12. 0012specialize beta_prefix_extend cc
  13. 0013specialize beta_prefix_extend x
  14. 0014cases beta_prefix_extend
  15. 0015cases beta_prefix_extend_witness
  16. 0016cases beta_prefix_extend_witness_witness
  17. 0017exists x1
  18. 0018exists x2
  19. 0019intro i
  20. 0020intro hi
  21. 0021have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists gap. gap + S i = l
  22. 0022specialize finite_lt_succ_eq_or_lt l
  23. 0023specialize finite_lt_succ_eq_or_lt i
  24. 0024apply finite_lt_succ_eq_or_lt
  25. 0025exact hi
  26. 0026cases hsplit
  27. 0027exists x
  28. 0028split
  29. 0029rewrite hsplit_left
  30. 0030rewrite hsplit_left
  31. 0031exact beta_prefix_extend_witness_witness_left
  32. 0032rewrite hsplit_left
  33. 0033rewrite hsplit_left
  34. 0034rewrite hsplit_left
  35. 0035rewrite hsplit_left
  36. 0036exact hchoice_witness
  37. 0037have hold : ∃ oldcount. BetaAt(cb,cc,i,oldcount) ∧ (∃ 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,oldcount))
    Exact native replay linehave hold : exists oldcount. ((((exists ff_h_rectangle_count_extend_old_entry. ff_h_rectangle_count_extend_old_entry + S (oldcount) = S ((S (i)) * cc)) /\ exists ff_q_rectangle_count_extend_old_entry. cb = ff_q_rectangle_count_extend_old_entry * S ((S (i)) * cc) + (oldcount))) /\ (exists erc_row_code_rectangle_count_extend_old_witness erc_row_scale_rectangle_count_extend_old_witness. ((forall eri_column_erc_rectangle_count_extend_old_witness_row. (exists eri_gap_erc_rectangle_count_extend_old_witness_row_bound. eri_gap_erc_rectangle_count_extend_old_witness_row_bound + S (eri_column_erc_rectangle_count_extend_old_witness_row) = k) -> exists eri_bit_erc_rectangle_count_extend_old_witness_row. ((((exists ff_h_eri_erc_rectangle_count_extend_old_witness_row_decoded. ff_h_eri_erc_rectangle_count_extend_old_witness_row_decoded + S (eri_bit_erc_rectangle_count_extend_old_witness_row) = S ((S (eri_column_erc_rectangle_count_extend_old_witness_row)) * erc_row_scale_rectangle_count_extend_old_witness)) /\ exists ff_q_eri_erc_rectangle_count_extend_old_witness_row_decoded. erc_row_code_rectangle_count_extend_old_witness = ff_q_eri_erc_rectangle_count_extend_old_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_extend_old_witness_row)) * erc_row_scale_rectangle_count_extend_old_witness) + (eri_bit_erc_rectangle_count_extend_old_witness_row))) /\ (((eri_bit_erc_rectangle_count_extend_old_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_extend_old_witness_row_choice_left. eri_gap_erc_rectangle_count_extend_old_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_rectangle_count_extend_old_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_extend_old_witness_row_choice_right. eri_gap_erc_rectangle_count_extend_old_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_old_witness_row) = q * S i))) \/ (eri_bit_erc_rectangle_count_extend_old_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_extend_old_witness_row_choice_right. eri_gap_erc_rectangle_count_extend_old_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_old_witness_row) = q * S i) /\ ~(exists eri_gap_erc_rectangle_count_extend_old_witness_row_choice_left. eri_gap_erc_rectangle_count_extend_old_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_rectangle_count_extend_old_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_extend_old_witness_count_sum ff_v_erc_rectangle_count_extend_old_witness_count_sum. ((((exists ff_h_erc_rectangle_count_extend_old_witness_count_sum_start. ff_h_erc_rectangle_count_extend_old_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_extend_old_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_old_witness_count_sum_start. ff_u_erc_rectangle_count_extend_old_witness_count_sum = ff_q_erc_rectangle_count_extend_old_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_extend_old_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_extend_old_witness_count_sum_terminal. ff_h_erc_rectangle_count_extend_old_witness_count_sum_terminal + S (oldcount) = S ((S (k)) * ff_v_erc_rectangle_count_extend_old_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_old_witness_count_sum_terminal. ff_u_erc_rectangle_count_extend_old_witness_count_sum = ff_q_erc_rectangle_count_extend_old_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_extend_old_witness_count_sum) + (oldcount))) /\ forall ff_i_erc_rectangle_count_extend_old_witness_count_sum. (exists ff_lt_erc_rectangle_count_extend_old_witness_count_sum_bound. ff_lt_erc_rectangle_count_extend_old_witness_count_sum_bound + S ff_i_erc_rectangle_count_extend_old_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_extend_old_witness_count_sum ff_r_erc_rectangle_count_extend_old_witness_count_sum ff_s_erc_rectangle_count_extend_old_witness_count_sum. ((((exists ff_h_erc_rectangle_count_extend_old_witness_count_sum_summand. ff_h_erc_rectangle_count_extend_old_witness_count_sum_summand + S (ff_a_erc_rectangle_count_extend_old_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_old_witness_count_sum)) * erc_row_scale_rectangle_count_extend_old_witness)) /\ exists ff_q_erc_rectangle_count_extend_old_witness_count_sum_summand. erc_row_code_rectangle_count_extend_old_witness = ff_q_erc_rectangle_count_extend_old_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_extend_old_witness_count_sum)) * erc_row_scale_rectangle_count_extend_old_witness) + (ff_a_erc_rectangle_count_extend_old_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_old_witness_count_sum_partial. ff_h_erc_rectangle_count_extend_old_witness_count_sum_partial + S (ff_r_erc_rectangle_count_extend_old_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_old_witness_count_sum)) * ff_v_erc_rectangle_count_extend_old_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_old_witness_count_sum_partial. ff_u_erc_rectangle_count_extend_old_witness_count_sum = ff_q_erc_rectangle_count_extend_old_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_extend_old_witness_count_sum)) * ff_v_erc_rectangle_count_extend_old_witness_count_sum) + (ff_r_erc_rectangle_count_extend_old_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_old_witness_count_sum_successor. ff_h_erc_rectangle_count_extend_old_witness_count_sum_successor + S (ff_s_erc_rectangle_count_extend_old_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_extend_old_witness_count_sum)) * ff_v_erc_rectangle_count_extend_old_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_old_witness_count_sum_successor. ff_u_erc_rectangle_count_extend_old_witness_count_sum = ff_q_erc_rectangle_count_extend_old_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_extend_old_witness_count_sum)) * ff_v_erc_rectangle_count_extend_old_witness_count_sum) + (ff_s_erc_rectangle_count_extend_old_witness_count_sum))) /\ ff_s_erc_rectangle_count_extend_old_witness_count_sum = ff_r_erc_rectangle_count_extend_old_witness_count_sum + ff_a_erc_rectangle_count_extend_old_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_extend_old_witness_count_bits. (exists ff_lt_erc_rectangle_count_extend_old_witness_count_bits_bound. ff_lt_erc_rectangle_count_extend_old_witness_count_bits_bound + S ff_i_erc_rectangle_count_extend_old_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_extend_old_witness_count_bits. ((((exists ff_h_erc_rectangle_count_extend_old_witness_count_bits_decoded. ff_h_erc_rectangle_count_extend_old_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_extend_old_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_extend_old_witness_count_bits)) * erc_row_scale_rectangle_count_extend_old_witness)) /\ exists ff_q_erc_rectangle_count_extend_old_witness_count_bits_decoded. erc_row_code_rectangle_count_extend_old_witness = ff_q_erc_rectangle_count_extend_old_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_extend_old_witness_count_bits)) * erc_row_scale_rectangle_count_extend_old_witness) + (ff_bit_erc_rectangle_count_extend_old_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_extend_old_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_extend_old_witness_count_bits = 1))))))))
  38. 0038specialize hprefix i
  39. 0039apply hprefix
  40. 0040exact hsplit_right
  41. 0041cases hold
  42. 0042cases hold_witness
  43. 0043exists x3
  44. 0044split
  45. 0045specialize beta_prefix_extend_witness_witness_right i
  46. 0046specialize beta_prefix_extend_witness_witness_right x3
  47. 0047apply beta_prefix_extend_witness_witness_right
  48. 0048exact hsplit_right
  49. 0049exact hold_witness_left
  50. 0050exact hold_witness_right