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. ∀ i. ∀ n. (∀ x. Lt(x,l) → ∃ y. BetaAt(cb,cc,x,y) ∧ (∃ z. ∃ m. (∀ j. Lt(j,k) → ∃ u. BetaAt(z,m,j,u) ∧ (u = 0 ∧ (Lt(q · S x,p · S j) ∧ ¬Lt(p · S j,q · S x)) ∨ u = 1 ∧ (Lt(p · S j,q · S x) ∧ ¬Lt(q · S x,p · S j)))) ∧ BitCount(z,m,k,y))) → Lt(i,l) → BetaAt(cb,cc,i,n) → ∃ x. ∃ y. (∀ z. Lt(z,k) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ m = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))) ∧ BitCount(x,y,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
18 occurrences
In local proof propositions
8 occurrences
Exact expanded native-PA statement
forall p q k cb cc l i n. (forall erc_row_rectangle_count_projection_prefix. (exists erc_lt_gap_rectangle_count_projection_prefix_bound. erc_lt_gap_rectangle_count_projection_prefix_bound + S (erc_row_rectangle_count_projection_prefix) = l) -> exists erc_count_rectangle_count_projection_prefix. ((((exists ff_h_erc_rectangle_count_projection_prefix_decoded. ff_h_erc_rectangle_count_projection_prefix_decoded + S (erc_count_rectangle_count_projection_prefix) = S ((S (erc_row_rectangle_count_projection_prefix)) * cc)) /\ exists ff_q_erc_rectangle_count_projection_prefix_decoded. cb = ff_q_erc_rectangle_count_projection_prefix_decoded * S ((S (erc_row_rectangle_count_projection_prefix)) * cc) + (erc_count_rectangle_count_projection_prefix))) /\ (exists erc_row_code_rectangle_count_projection_prefix_witness erc_row_scale_rectangle_count_projection_prefix_witness. ((forall eri_column_erc_rectangle_count_projection_prefix_witness_row. (exists eri_gap_erc_rectangle_count_projection_prefix_witness_row_bound. eri_gap_erc_rectangle_count_projection_prefix_witness_row_bound + S (eri_column_erc_rectangle_count_projection_prefix_witness_row) = k) -> exists eri_bit_erc_rectangle_count_projection_prefix_witness_row. ((((exists ff_h_eri_erc_rectangle_count_projection_prefix_witness_row_decoded. ff_h_eri_erc_rectangle_count_projection_prefix_witness_row_decoded + S (eri_bit_erc_rectangle_count_projection_prefix_witness_row) = S ((S (eri_column_erc_rectangle_count_projection_prefix_witness_row)) * erc_row_scale_rectangle_count_projection_prefix_witness)) /\ exists ff_q_eri_erc_rectangle_count_projection_prefix_witness_row_decoded. erc_row_code_rectangle_count_projection_prefix_witness = ff_q_eri_erc_rectangle_count_projection_prefix_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_projection_prefix_witness_row)) * erc_row_scale_rectangle_count_projection_prefix_witness) + (eri_bit_erc_rectangle_count_projection_prefix_witness_row))) /\ (((eri_bit_erc_rectangle_count_projection_prefix_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_projection_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_projection_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_projection_prefix) = p * S eri_column_erc_rectangle_count_projection_prefix_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_projection_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_projection_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_projection_prefix_witness_row) = q * S erc_row_rectangle_count_projection_prefix))) \/ (eri_bit_erc_rectangle_count_projection_prefix_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_projection_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_projection_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_projection_prefix_witness_row) = q * S erc_row_rectangle_count_projection_prefix) /\ ~(exists eri_gap_erc_rectangle_count_projection_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_projection_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_projection_prefix) = p * S eri_column_erc_rectangle_count_projection_prefix_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_projection_prefix_witness_count_sum ff_v_erc_rectangle_count_projection_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_projection_prefix_witness_count_sum_start. ff_h_erc_rectangle_count_projection_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_projection_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_projection_prefix_witness_count_sum_start. ff_u_erc_rectangle_count_projection_prefix_witness_count_sum = ff_q_erc_rectangle_count_projection_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_projection_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_projection_prefix_witness_count_sum_terminal. ff_h_erc_rectangle_count_projection_prefix_witness_count_sum_terminal + S (erc_count_rectangle_count_projection_prefix) = S ((S (k)) * ff_v_erc_rectangle_count_projection_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_projection_prefix_witness_count_sum_terminal. ff_u_erc_rectangle_count_projection_prefix_witness_count_sum = ff_q_erc_rectangle_count_projection_prefix_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_projection_prefix_witness_count_sum) + (erc_count_rectangle_count_projection_prefix))) /\ forall ff_i_erc_rectangle_count_projection_prefix_witness_count_sum. (exists ff_lt_erc_rectangle_count_projection_prefix_witness_count_sum_bound. ff_lt_erc_rectangle_count_projection_prefix_witness_count_sum_bound + S ff_i_erc_rectangle_count_projection_prefix_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_projection_prefix_witness_count_sum ff_r_erc_rectangle_count_projection_prefix_witness_count_sum ff_s_erc_rectangle_count_projection_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_projection_prefix_witness_count_sum_summand. ff_h_erc_rectangle_count_projection_prefix_witness_count_sum_summand + S (ff_a_erc_rectangle_count_projection_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_projection_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_projection_prefix_witness)) /\ exists ff_q_erc_rectangle_count_projection_prefix_witness_count_sum_summand. erc_row_code_rectangle_count_projection_prefix_witness = ff_q_erc_rectangle_count_projection_prefix_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_projection_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_projection_prefix_witness) + (ff_a_erc_rectangle_count_projection_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_projection_prefix_witness_count_sum_partial. ff_h_erc_rectangle_count_projection_prefix_witness_count_sum_partial + S (ff_r_erc_rectangle_count_projection_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_projection_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_projection_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_projection_prefix_witness_count_sum_partial. ff_u_erc_rectangle_count_projection_prefix_witness_count_sum = ff_q_erc_rectangle_count_projection_prefix_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_projection_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_projection_prefix_witness_count_sum) + (ff_r_erc_rectangle_count_projection_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_projection_prefix_witness_count_sum_successor. ff_h_erc_rectangle_count_projection_prefix_witness_count_sum_successor + S (ff_s_erc_rectangle_count_projection_prefix_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_projection_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_projection_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_projection_prefix_witness_count_sum_successor. ff_u_erc_rectangle_count_projection_prefix_witness_count_sum = ff_q_erc_rectangle_count_projection_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_projection_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_projection_prefix_witness_count_sum) + (ff_s_erc_rectangle_count_projection_prefix_witness_count_sum))) /\ ff_s_erc_rectangle_count_projection_prefix_witness_count_sum = ff_r_erc_rectangle_count_projection_prefix_witness_count_sum + ff_a_erc_rectangle_count_projection_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_projection_prefix_witness_count_bits. (exists ff_lt_erc_rectangle_count_projection_prefix_witness_count_bits_bound. ff_lt_erc_rectangle_count_projection_prefix_witness_count_bits_bound + S ff_i_erc_rectangle_count_projection_prefix_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_projection_prefix_witness_count_bits. ((((exists ff_h_erc_rectangle_count_projection_prefix_witness_count_bits_decoded. ff_h_erc_rectangle_count_projection_prefix_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_projection_prefix_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_projection_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_projection_prefix_witness)) /\ exists ff_q_erc_rectangle_count_projection_prefix_witness_count_bits_decoded. erc_row_code_rectangle_count_projection_prefix_witness = ff_q_erc_rectangle_count_projection_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_projection_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_projection_prefix_witness) + (ff_bit_erc_rectangle_count_projection_prefix_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_projection_prefix_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_projection_prefix_witness_count_bits = 1))))))))) -> (exists erc_lt_gap_rectangle_count_projection_bound. erc_lt_gap_rectangle_count_projection_bound + S (i) = l) -> (((exists ff_h_rectangle_count_projection_entry. ff_h_rectangle_count_projection_entry + S (n) = S ((S (i)) * cc)) /\ exists ff_q_rectangle_count_projection_entry. cb = ff_q_rectangle_count_projection_entry * S ((S (i)) * cc) + (n))) -> (exists erc_row_code_rectangle_count_projection_witness erc_row_scale_rectangle_count_projection_witness. ((forall eri_column_erc_rectangle_count_projection_witness_row. (exists eri_gap_erc_rectangle_count_projection_witness_row_bound. eri_gap_erc_rectangle_count_projection_witness_row_bound + S (eri_column_erc_rectangle_count_projection_witness_row) = k) -> exists eri_bit_erc_rectangle_count_projection_witness_row. ((((exists ff_h_eri_erc_rectangle_count_projection_witness_row_decoded. ff_h_eri_erc_rectangle_count_projection_witness_row_decoded + S (eri_bit_erc_rectangle_count_projection_witness_row) = S ((S (eri_column_erc_rectangle_count_projection_witness_row)) * erc_row_scale_rectangle_count_projection_witness)) /\ exists ff_q_eri_erc_rectangle_count_projection_witness_row_decoded. erc_row_code_rectangle_count_projection_witness = ff_q_eri_erc_rectangle_count_projection_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_projection_witness_row)) * erc_row_scale_rectangle_count_projection_witness) + (eri_bit_erc_rectangle_count_projection_witness_row))) /\ (((eri_bit_erc_rectangle_count_projection_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_projection_witness_row_choice_left. eri_gap_erc_rectangle_count_projection_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_rectangle_count_projection_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_projection_witness_row_choice_right. eri_gap_erc_rectangle_count_projection_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_projection_witness_row) = q * S i))) \/ (eri_bit_erc_rectangle_count_projection_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_projection_witness_row_choice_right. eri_gap_erc_rectangle_count_projection_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_projection_witness_row) = q * S i) /\ ~(exists eri_gap_erc_rectangle_count_projection_witness_row_choice_left. eri_gap_erc_rectangle_count_projection_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_rectangle_count_projection_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_projection_witness_count_sum ff_v_erc_rectangle_count_projection_witness_count_sum. ((((exists ff_h_erc_rectangle_count_projection_witness_count_sum_start. ff_h_erc_rectangle_count_projection_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_projection_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_projection_witness_count_sum_start. ff_u_erc_rectangle_count_projection_witness_count_sum = ff_q_erc_rectangle_count_projection_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_projection_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_projection_witness_count_sum_terminal. ff_h_erc_rectangle_count_projection_witness_count_sum_terminal + S (n) = S ((S (k)) * ff_v_erc_rectangle_count_projection_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_projection_witness_count_sum_terminal. ff_u_erc_rectangle_count_projection_witness_count_sum = ff_q_erc_rectangle_count_projection_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_projection_witness_count_sum) + (n))) /\ forall ff_i_erc_rectangle_count_projection_witness_count_sum. (exists ff_lt_erc_rectangle_count_projection_witness_count_sum_bound. ff_lt_erc_rectangle_count_projection_witness_count_sum_bound + S ff_i_erc_rectangle_count_projection_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_projection_witness_count_sum ff_r_erc_rectangle_count_projection_witness_count_sum ff_s_erc_rectangle_count_projection_witness_count_sum. ((((exists ff_h_erc_rectangle_count_projection_witness_count_sum_summand. ff_h_erc_rectangle_count_projection_witness_count_sum_summand + S (ff_a_erc_rectangle_count_projection_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_projection_witness_count_sum)) * erc_row_scale_rectangle_count_projection_witness)) /\ exists ff_q_erc_rectangle_count_projection_witness_count_sum_summand. erc_row_code_rectangle_count_projection_witness = ff_q_erc_rectangle_count_projection_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_projection_witness_count_sum)) * erc_row_scale_rectangle_count_projection_witness) + (ff_a_erc_rectangle_count_projection_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_projection_witness_count_sum_partial. ff_h_erc_rectangle_count_projection_witness_count_sum_partial + S (ff_r_erc_rectangle_count_projection_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_projection_witness_count_sum)) * ff_v_erc_rectangle_count_projection_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_projection_witness_count_sum_partial. ff_u_erc_rectangle_count_projection_witness_count_sum = ff_q_erc_rectangle_count_projection_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_projection_witness_count_sum)) * ff_v_erc_rectangle_count_projection_witness_count_sum) + (ff_r_erc_rectangle_count_projection_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_projection_witness_count_sum_successor. ff_h_erc_rectangle_count_projection_witness_count_sum_successor + S (ff_s_erc_rectangle_count_projection_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_projection_witness_count_sum)) * ff_v_erc_rectangle_count_projection_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_projection_witness_count_sum_successor. ff_u_erc_rectangle_count_projection_witness_count_sum = ff_q_erc_rectangle_count_projection_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_projection_witness_count_sum)) * ff_v_erc_rectangle_count_projection_witness_count_sum) + (ff_s_erc_rectangle_count_projection_witness_count_sum))) /\ ff_s_erc_rectangle_count_projection_witness_count_sum = ff_r_erc_rectangle_count_projection_witness_count_sum + ff_a_erc_rectangle_count_projection_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_projection_witness_count_bits. (exists ff_lt_erc_rectangle_count_projection_witness_count_bits_bound. ff_lt_erc_rectangle_count_projection_witness_count_bits_bound + S ff_i_erc_rectangle_count_projection_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_projection_witness_count_bits. ((((exists ff_h_erc_rectangle_count_projection_witness_count_bits_decoded. ff_h_erc_rectangle_count_projection_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_projection_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_projection_witness_count_bits)) * erc_row_scale_rectangle_count_projection_witness)) /\ exists ff_q_erc_rectangle_count_projection_witness_count_bits_decoded. erc_row_code_rectangle_count_projection_witness = ff_q_erc_rectangle_count_projection_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_projection_witness_count_bits)) * erc_row_scale_rectangle_count_projection_witness) + (ff_bit_erc_rectangle_count_projection_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_projection_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_projection_witness_count_bits = 1)))))))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
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
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 (1)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–11
Work with arbitrary variables or the premises of the current implication.
- L11
intro hentry
03Establish hstoredL12–15
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.
- L12
have hstored : ∃ stored. BetaAt(cb,cc,i,stored) ∧ (∃ 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,stored))Definitions: BetaAt(cb,cc,i,stored)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,stored)Original native command in the exact edition - L13
specialize hprefix i - L14
apply hprefix - L15
exact hi
04Separate the logical casesL16–17
05Establish heqL18–27
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
06Calculate and transport equalitiesL28–28
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L28
rewrite heq at hstored_witness_right
07Use earlier factsL29–29
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L29
exact hstored_witness_right
Original defined command ledger · 29 lines
- 0001
intro p - 0002
intro q - 0003
intro k - 0004
intro cb - 0005
intro cc - 0006
intro l - 0007
intro i - 0008
intro n - 0009
intro hprefix - 0010
intro hi - 0011
intro hentry - 0012
have hstored : ∃ stored. BetaAt(cb,cc,i,stored) ∧ (∃ 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,stored))Exact native replay line
have hstored : exists stored. ((((exists ff_h_rectangle_count_projection_stored. ff_h_rectangle_count_projection_stored + S (stored) = S ((S (i)) * cc)) /\ exists ff_q_rectangle_count_projection_stored. cb = ff_q_rectangle_count_projection_stored * S ((S (i)) * cc) + (stored))) /\ (exists erc_row_code_rectangle_count_projection_stored_witness erc_row_scale_rectangle_count_projection_stored_witness. ((forall eri_column_erc_rectangle_count_projection_stored_witness_row. (exists eri_gap_erc_rectangle_count_projection_stored_witness_row_bound. eri_gap_erc_rectangle_count_projection_stored_witness_row_bound + S (eri_column_erc_rectangle_count_projection_stored_witness_row) = k) -> exists eri_bit_erc_rectangle_count_projection_stored_witness_row. ((((exists ff_h_eri_erc_rectangle_count_projection_stored_witness_row_decoded. ff_h_eri_erc_rectangle_count_projection_stored_witness_row_decoded + S (eri_bit_erc_rectangle_count_projection_stored_witness_row) = S ((S (eri_column_erc_rectangle_count_projection_stored_witness_row)) * erc_row_scale_rectangle_count_projection_stored_witness)) /\ exists ff_q_eri_erc_rectangle_count_projection_stored_witness_row_decoded. erc_row_code_rectangle_count_projection_stored_witness = ff_q_eri_erc_rectangle_count_projection_stored_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_projection_stored_witness_row)) * erc_row_scale_rectangle_count_projection_stored_witness) + (eri_bit_erc_rectangle_count_projection_stored_witness_row))) /\ (((eri_bit_erc_rectangle_count_projection_stored_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_projection_stored_witness_row_choice_left. eri_gap_erc_rectangle_count_projection_stored_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_rectangle_count_projection_stored_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_projection_stored_witness_row_choice_right. eri_gap_erc_rectangle_count_projection_stored_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_projection_stored_witness_row) = q * S i))) \/ (eri_bit_erc_rectangle_count_projection_stored_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_projection_stored_witness_row_choice_right. eri_gap_erc_rectangle_count_projection_stored_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_projection_stored_witness_row) = q * S i) /\ ~(exists eri_gap_erc_rectangle_count_projection_stored_witness_row_choice_left. eri_gap_erc_rectangle_count_projection_stored_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_rectangle_count_projection_stored_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_projection_stored_witness_count_sum ff_v_erc_rectangle_count_projection_stored_witness_count_sum. ((((exists ff_h_erc_rectangle_count_projection_stored_witness_count_sum_start. ff_h_erc_rectangle_count_projection_stored_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_projection_stored_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_projection_stored_witness_count_sum_start. ff_u_erc_rectangle_count_projection_stored_witness_count_sum = ff_q_erc_rectangle_count_projection_stored_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_projection_stored_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_projection_stored_witness_count_sum_terminal. ff_h_erc_rectangle_count_projection_stored_witness_count_sum_terminal + S (stored) = S ((S (k)) * ff_v_erc_rectangle_count_projection_stored_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_projection_stored_witness_count_sum_terminal. ff_u_erc_rectangle_count_projection_stored_witness_count_sum = ff_q_erc_rectangle_count_projection_stored_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_projection_stored_witness_count_sum) + (stored))) /\ forall ff_i_erc_rectangle_count_projection_stored_witness_count_sum. (exists ff_lt_erc_rectangle_count_projection_stored_witness_count_sum_bound. ff_lt_erc_rectangle_count_projection_stored_witness_count_sum_bound + S ff_i_erc_rectangle_count_projection_stored_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_projection_stored_witness_count_sum ff_r_erc_rectangle_count_projection_stored_witness_count_sum ff_s_erc_rectangle_count_projection_stored_witness_count_sum. ((((exists ff_h_erc_rectangle_count_projection_stored_witness_count_sum_summand. ff_h_erc_rectangle_count_projection_stored_witness_count_sum_summand + S (ff_a_erc_rectangle_count_projection_stored_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_projection_stored_witness_count_sum)) * erc_row_scale_rectangle_count_projection_stored_witness)) /\ exists ff_q_erc_rectangle_count_projection_stored_witness_count_sum_summand. erc_row_code_rectangle_count_projection_stored_witness = ff_q_erc_rectangle_count_projection_stored_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_projection_stored_witness_count_sum)) * erc_row_scale_rectangle_count_projection_stored_witness) + (ff_a_erc_rectangle_count_projection_stored_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_projection_stored_witness_count_sum_partial. ff_h_erc_rectangle_count_projection_stored_witness_count_sum_partial + S (ff_r_erc_rectangle_count_projection_stored_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_projection_stored_witness_count_sum)) * ff_v_erc_rectangle_count_projection_stored_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_projection_stored_witness_count_sum_partial. ff_u_erc_rectangle_count_projection_stored_witness_count_sum = ff_q_erc_rectangle_count_projection_stored_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_projection_stored_witness_count_sum)) * ff_v_erc_rectangle_count_projection_stored_witness_count_sum) + (ff_r_erc_rectangle_count_projection_stored_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_projection_stored_witness_count_sum_successor. ff_h_erc_rectangle_count_projection_stored_witness_count_sum_successor + S (ff_s_erc_rectangle_count_projection_stored_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_projection_stored_witness_count_sum)) * ff_v_erc_rectangle_count_projection_stored_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_projection_stored_witness_count_sum_successor. ff_u_erc_rectangle_count_projection_stored_witness_count_sum = ff_q_erc_rectangle_count_projection_stored_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_projection_stored_witness_count_sum)) * ff_v_erc_rectangle_count_projection_stored_witness_count_sum) + (ff_s_erc_rectangle_count_projection_stored_witness_count_sum))) /\ ff_s_erc_rectangle_count_projection_stored_witness_count_sum = ff_r_erc_rectangle_count_projection_stored_witness_count_sum + ff_a_erc_rectangle_count_projection_stored_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_projection_stored_witness_count_bits. (exists ff_lt_erc_rectangle_count_projection_stored_witness_count_bits_bound. ff_lt_erc_rectangle_count_projection_stored_witness_count_bits_bound + S ff_i_erc_rectangle_count_projection_stored_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_projection_stored_witness_count_bits. ((((exists ff_h_erc_rectangle_count_projection_stored_witness_count_bits_decoded. ff_h_erc_rectangle_count_projection_stored_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_projection_stored_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_projection_stored_witness_count_bits)) * erc_row_scale_rectangle_count_projection_stored_witness)) /\ exists ff_q_erc_rectangle_count_projection_stored_witness_count_bits_decoded. erc_row_code_rectangle_count_projection_stored_witness = ff_q_erc_rectangle_count_projection_stored_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_projection_stored_witness_count_bits)) * erc_row_scale_rectangle_count_projection_stored_witness) + (ff_bit_erc_rectangle_count_projection_stored_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_projection_stored_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_projection_stored_witness_count_bits = 1)))))))) - 0013
specialize hprefix i - 0014
apply hprefix - 0015
exact hi - 0016
cases hstored - 0017
cases hstored_witness - 0018
have heq : x = n - 0019
specialize beta_at_unique cb - 0020
specialize beta_at_unique cc - 0021
specialize beta_at_unique i - 0022
specialize beta_at_unique x - 0023
specialize beta_at_unique n - 0024
apply beta_at_unique - 0025
exact hstored_witness_left - 0026
exact hentry - 0027
rewrite heq at hstored_witness_right - 0028
rewrite heq at hstored_witness_right - 0029
exact hstored_witness_right