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. ∀ h. ∀ k. ∀ i. ∀ tb. ∀ tc. ∀ qb. ∀ qc. ∀ ub. ∀ uc. ∀ cb. ∀ cc. ∀ d. p = 2 · h + 1 → q = 2 · k + 1 → Prime(p) → Prime(q) → ¬p = q → Lt(i,h) → (∀ x. ∀ y. Lt(x,h) → BetaAt(tb,tc,x,y) → y = q · (1 + x)) → DivisionPrefix(p,tb,tc,qb,qc,ub,uc,h) → (∀ x. Lt(x,h) → ∃ y. BetaAt(cb,cc,x,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,k) → ∃ j. BetaAt(z,n,m,j) ∧ (j = 0 ∧ (Lt(q · S x,p · S m) ∧ ¬Lt(p · S m,q · S x)) ∨ j = 1 ∧ (Lt(p · S m,q · S x) ∧ ¬Lt(q · S x,p · S m)))) ∧ BitCount(z,n,k,y))) → BetaAt(qb,qc,i,d) → BetaAt(cb,cc,i,d)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
17 occurrences
In local proof propositions
8 occurrences
Exact expanded native-PA statement
forall p q h k i tb tc qb qc ub uc cb cc d. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_outer_sum_bridge_prime_p frp_prime_right_outer_sum_bridge_prime_p. p = frp_prime_left_outer_sum_bridge_prime_p * frp_prime_right_outer_sum_bridge_prime_p -> frp_prime_left_outer_sum_bridge_prime_p = 1 \/ frp_prime_right_outer_sum_bridge_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_outer_sum_bridge_prime_q frp_prime_right_outer_sum_bridge_prime_q. q = frp_prime_left_outer_sum_bridge_prime_q * frp_prime_right_outer_sum_bridge_prime_q -> frp_prime_left_outer_sum_bridge_prime_q = 1 \/ frp_prime_right_outer_sum_bridge_prime_q = 1)) -> ~(p = q) -> (exists edt_lt_gap_outer_sum_bridge_row_bound. edt_lt_gap_outer_sum_bridge_row_bound + S (i) = h) -> (forall esd_index_outer_sum_bridge_scaled esd_value_outer_sum_bridge_scaled. (exists esd_gap_outer_sum_bridge_scaled. esd_gap_outer_sum_bridge_scaled + S esd_index_outer_sum_bridge_scaled = h) -> (((exists ff_h_esd_outer_sum_bridge_scaled_decoded. ff_h_esd_outer_sum_bridge_scaled_decoded + S (esd_value_outer_sum_bridge_scaled) = S ((S (esd_index_outer_sum_bridge_scaled)) * tc)) /\ exists ff_q_esd_outer_sum_bridge_scaled_decoded. tb = ff_q_esd_outer_sum_bridge_scaled_decoded * S ((S (esd_index_outer_sum_bridge_scaled)) * tc) + (esd_value_outer_sum_bridge_scaled))) -> esd_value_outer_sum_bridge_scaled = q * (1 + esd_index_outer_sum_bridge_scaled)) -> (forall fdp_index_outer_sum_bridge_division. (exists gsp_lt_gap_outer_sum_bridge_division_index_bound. gsp_lt_gap_outer_sum_bridge_division_index_bound + S fdp_index_outer_sum_bridge_division = h) -> exists fdp_value_outer_sum_bridge_division fdp_quotient_outer_sum_bridge_division fdp_remainder_outer_sum_bridge_division. (((exists ff_h_fdp_outer_sum_bridge_division_source. ff_h_fdp_outer_sum_bridge_division_source + S (fdp_value_outer_sum_bridge_division) = S ((S (fdp_index_outer_sum_bridge_division)) * tc)) /\ exists ff_q_fdp_outer_sum_bridge_division_source. tb = ff_q_fdp_outer_sum_bridge_division_source * S ((S (fdp_index_outer_sum_bridge_division)) * tc) + (fdp_value_outer_sum_bridge_division))) /\ ((((exists ff_h_fdp_outer_sum_bridge_division_quotient_entry. ff_h_fdp_outer_sum_bridge_division_quotient_entry + S (fdp_quotient_outer_sum_bridge_division) = S ((S (fdp_index_outer_sum_bridge_division)) * qc)) /\ exists ff_q_fdp_outer_sum_bridge_division_quotient_entry. qb = ff_q_fdp_outer_sum_bridge_division_quotient_entry * S ((S (fdp_index_outer_sum_bridge_division)) * qc) + (fdp_quotient_outer_sum_bridge_division))) /\ ((((exists ff_h_fdp_outer_sum_bridge_division_remainder_entry. ff_h_fdp_outer_sum_bridge_division_remainder_entry + S (fdp_remainder_outer_sum_bridge_division) = S ((S (fdp_index_outer_sum_bridge_division)) * uc)) /\ exists ff_q_fdp_outer_sum_bridge_division_remainder_entry. ub = ff_q_fdp_outer_sum_bridge_division_remainder_entry * S ((S (fdp_index_outer_sum_bridge_division)) * uc) + (fdp_remainder_outer_sum_bridge_division))) /\ (fdp_value_outer_sum_bridge_division = p * fdp_quotient_outer_sum_bridge_division + fdp_remainder_outer_sum_bridge_division /\ (exists gsp_lt_gap_outer_sum_bridge_division_remainder_bound. gsp_lt_gap_outer_sum_bridge_division_remainder_bound + S fdp_remainder_outer_sum_bridge_division = p))))) -> (forall erc_row_outer_sum_bridge_rectangle. (exists erc_lt_gap_outer_sum_bridge_rectangle_bound. erc_lt_gap_outer_sum_bridge_rectangle_bound + S (erc_row_outer_sum_bridge_rectangle) = h) -> exists erc_count_outer_sum_bridge_rectangle. ((((exists ff_h_erc_outer_sum_bridge_rectangle_decoded. ff_h_erc_outer_sum_bridge_rectangle_decoded + S (erc_count_outer_sum_bridge_rectangle) = S ((S (erc_row_outer_sum_bridge_rectangle)) * cc)) /\ exists ff_q_erc_outer_sum_bridge_rectangle_decoded. cb = ff_q_erc_outer_sum_bridge_rectangle_decoded * S ((S (erc_row_outer_sum_bridge_rectangle)) * cc) + (erc_count_outer_sum_bridge_rectangle))) /\ (exists erc_row_code_outer_sum_bridge_rectangle_witness erc_row_scale_outer_sum_bridge_rectangle_witness. ((forall eri_column_erc_outer_sum_bridge_rectangle_witness_row. (exists eri_gap_erc_outer_sum_bridge_rectangle_witness_row_bound. eri_gap_erc_outer_sum_bridge_rectangle_witness_row_bound + S (eri_column_erc_outer_sum_bridge_rectangle_witness_row) = k) -> exists eri_bit_erc_outer_sum_bridge_rectangle_witness_row. ((((exists ff_h_eri_erc_outer_sum_bridge_rectangle_witness_row_decoded. ff_h_eri_erc_outer_sum_bridge_rectangle_witness_row_decoded + S (eri_bit_erc_outer_sum_bridge_rectangle_witness_row) = S ((S (eri_column_erc_outer_sum_bridge_rectangle_witness_row)) * erc_row_scale_outer_sum_bridge_rectangle_witness)) /\ exists ff_q_eri_erc_outer_sum_bridge_rectangle_witness_row_decoded. erc_row_code_outer_sum_bridge_rectangle_witness = ff_q_eri_erc_outer_sum_bridge_rectangle_witness_row_decoded * S ((S (eri_column_erc_outer_sum_bridge_rectangle_witness_row)) * erc_row_scale_outer_sum_bridge_rectangle_witness) + (eri_bit_erc_outer_sum_bridge_rectangle_witness_row))) /\ (((eri_bit_erc_outer_sum_bridge_rectangle_witness_row = 0 /\ ((exists eri_gap_erc_outer_sum_bridge_rectangle_witness_row_choice_left. eri_gap_erc_outer_sum_bridge_rectangle_witness_row_choice_left + S (q * S erc_row_outer_sum_bridge_rectangle) = p * S eri_column_erc_outer_sum_bridge_rectangle_witness_row) /\ ~(exists eri_gap_erc_outer_sum_bridge_rectangle_witness_row_choice_right. eri_gap_erc_outer_sum_bridge_rectangle_witness_row_choice_right + S (p * S eri_column_erc_outer_sum_bridge_rectangle_witness_row) = q * S erc_row_outer_sum_bridge_rectangle))) \/ (eri_bit_erc_outer_sum_bridge_rectangle_witness_row = 1 /\ ((exists eri_gap_erc_outer_sum_bridge_rectangle_witness_row_choice_right. eri_gap_erc_outer_sum_bridge_rectangle_witness_row_choice_right + S (p * S eri_column_erc_outer_sum_bridge_rectangle_witness_row) = q * S erc_row_outer_sum_bridge_rectangle) /\ ~(exists eri_gap_erc_outer_sum_bridge_rectangle_witness_row_choice_left. eri_gap_erc_outer_sum_bridge_rectangle_witness_row_choice_left + S (q * S erc_row_outer_sum_bridge_rectangle) = p * S eri_column_erc_outer_sum_bridge_rectangle_witness_row))))))) /\ (((exists ff_u_erc_outer_sum_bridge_rectangle_witness_count_sum ff_v_erc_outer_sum_bridge_rectangle_witness_count_sum. ((((exists ff_h_erc_outer_sum_bridge_rectangle_witness_count_sum_start. ff_h_erc_outer_sum_bridge_rectangle_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_outer_sum_bridge_rectangle_witness_count_sum)) /\ exists ff_q_erc_outer_sum_bridge_rectangle_witness_count_sum_start. ff_u_erc_outer_sum_bridge_rectangle_witness_count_sum = ff_q_erc_outer_sum_bridge_rectangle_witness_count_sum_start * S ((S (0)) * ff_v_erc_outer_sum_bridge_rectangle_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_outer_sum_bridge_rectangle_witness_count_sum_terminal. ff_h_erc_outer_sum_bridge_rectangle_witness_count_sum_terminal + S (erc_count_outer_sum_bridge_rectangle) = S ((S (k)) * ff_v_erc_outer_sum_bridge_rectangle_witness_count_sum)) /\ exists ff_q_erc_outer_sum_bridge_rectangle_witness_count_sum_terminal. ff_u_erc_outer_sum_bridge_rectangle_witness_count_sum = ff_q_erc_outer_sum_bridge_rectangle_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_outer_sum_bridge_rectangle_witness_count_sum) + (erc_count_outer_sum_bridge_rectangle))) /\ forall ff_i_erc_outer_sum_bridge_rectangle_witness_count_sum. (exists ff_lt_erc_outer_sum_bridge_rectangle_witness_count_sum_bound. ff_lt_erc_outer_sum_bridge_rectangle_witness_count_sum_bound + S ff_i_erc_outer_sum_bridge_rectangle_witness_count_sum = k) -> exists ff_a_erc_outer_sum_bridge_rectangle_witness_count_sum ff_r_erc_outer_sum_bridge_rectangle_witness_count_sum ff_s_erc_outer_sum_bridge_rectangle_witness_count_sum. ((((exists ff_h_erc_outer_sum_bridge_rectangle_witness_count_sum_summand. ff_h_erc_outer_sum_bridge_rectangle_witness_count_sum_summand + S (ff_a_erc_outer_sum_bridge_rectangle_witness_count_sum) = S ((S (ff_i_erc_outer_sum_bridge_rectangle_witness_count_sum)) * erc_row_scale_outer_sum_bridge_rectangle_witness)) /\ exists ff_q_erc_outer_sum_bridge_rectangle_witness_count_sum_summand. erc_row_code_outer_sum_bridge_rectangle_witness = ff_q_erc_outer_sum_bridge_rectangle_witness_count_sum_summand * S ((S (ff_i_erc_outer_sum_bridge_rectangle_witness_count_sum)) * erc_row_scale_outer_sum_bridge_rectangle_witness) + (ff_a_erc_outer_sum_bridge_rectangle_witness_count_sum))) /\ ((((exists ff_h_erc_outer_sum_bridge_rectangle_witness_count_sum_partial. ff_h_erc_outer_sum_bridge_rectangle_witness_count_sum_partial + S (ff_r_erc_outer_sum_bridge_rectangle_witness_count_sum) = S ((S (ff_i_erc_outer_sum_bridge_rectangle_witness_count_sum)) * ff_v_erc_outer_sum_bridge_rectangle_witness_count_sum)) /\ exists ff_q_erc_outer_sum_bridge_rectangle_witness_count_sum_partial. ff_u_erc_outer_sum_bridge_rectangle_witness_count_sum = ff_q_erc_outer_sum_bridge_rectangle_witness_count_sum_partial * S ((S (ff_i_erc_outer_sum_bridge_rectangle_witness_count_sum)) * ff_v_erc_outer_sum_bridge_rectangle_witness_count_sum) + (ff_r_erc_outer_sum_bridge_rectangle_witness_count_sum))) /\ ((((exists ff_h_erc_outer_sum_bridge_rectangle_witness_count_sum_successor. ff_h_erc_outer_sum_bridge_rectangle_witness_count_sum_successor + S (ff_s_erc_outer_sum_bridge_rectangle_witness_count_sum) = S ((S (S ff_i_erc_outer_sum_bridge_rectangle_witness_count_sum)) * ff_v_erc_outer_sum_bridge_rectangle_witness_count_sum)) /\ exists ff_q_erc_outer_sum_bridge_rectangle_witness_count_sum_successor. ff_u_erc_outer_sum_bridge_rectangle_witness_count_sum = ff_q_erc_outer_sum_bridge_rectangle_witness_count_sum_successor * S ((S (S ff_i_erc_outer_sum_bridge_rectangle_witness_count_sum)) * ff_v_erc_outer_sum_bridge_rectangle_witness_count_sum) + (ff_s_erc_outer_sum_bridge_rectangle_witness_count_sum))) /\ ff_s_erc_outer_sum_bridge_rectangle_witness_count_sum = ff_r_erc_outer_sum_bridge_rectangle_witness_count_sum + ff_a_erc_outer_sum_bridge_rectangle_witness_count_sum)))))) /\ (forall ff_i_erc_outer_sum_bridge_rectangle_witness_count_bits. (exists ff_lt_erc_outer_sum_bridge_rectangle_witness_count_bits_bound. ff_lt_erc_outer_sum_bridge_rectangle_witness_count_bits_bound + S ff_i_erc_outer_sum_bridge_rectangle_witness_count_bits = k) -> exists ff_bit_erc_outer_sum_bridge_rectangle_witness_count_bits. ((((exists ff_h_erc_outer_sum_bridge_rectangle_witness_count_bits_decoded. ff_h_erc_outer_sum_bridge_rectangle_witness_count_bits_decoded + S (ff_bit_erc_outer_sum_bridge_rectangle_witness_count_bits) = S ((S (ff_i_erc_outer_sum_bridge_rectangle_witness_count_bits)) * erc_row_scale_outer_sum_bridge_rectangle_witness)) /\ exists ff_q_erc_outer_sum_bridge_rectangle_witness_count_bits_decoded. erc_row_code_outer_sum_bridge_rectangle_witness = ff_q_erc_outer_sum_bridge_rectangle_witness_count_bits_decoded * S ((S (ff_i_erc_outer_sum_bridge_rectangle_witness_count_bits)) * erc_row_scale_outer_sum_bridge_rectangle_witness) + (ff_bit_erc_outer_sum_bridge_rectangle_witness_count_bits))) /\ (ff_bit_erc_outer_sum_bridge_rectangle_witness_count_bits = 0 \/ ff_bit_erc_outer_sum_bridge_rectangle_witness_count_bits = 1))))))))) -> (((exists ff_h_outer_sum_bridge_quotient_entry. ff_h_outer_sum_bridge_quotient_entry + S (d) = S ((S (i)) * qc)) /\ exists ff_q_outer_sum_bridge_quotient_entry. qb = ff_q_outer_sum_bridge_quotient_entry * S ((S (i)) * qc) + (d))) -> (((exists ff_h_outer_sum_bridge_rectangle_entry. ff_h_outer_sum_bridge_rectangle_entry + S (d) = S ((S (i)) * cc)) /\ exists ff_q_outer_sum_bridge_rectangle_entry. cb = ff_q_outer_sum_bridge_rectangle_entry * S ((S (i)) * cc) + (d)))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–20
03Fix variables and assumptionsL21–24
04Establish hstoredL25–28
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hrectangle.
- L25
have hstored : ∃ n. 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))Definitions: BetaAt(cb,cc,i,n)Lt(z,k)BetaAt(x,y,z,m)Lt(q · S i,p · S z)Lt(p · S z,q · S i)BitCount(x,y,k,n)Original native command in the exact edition - L26
specialize hrectangle i - L27
apply hrectangle - L28
exact hi
05Separate the logical casesL29–30
06Establish hndL31–40
Establish this local claim before using it. It is not an additional assumption.
- L31
have hnd : x = d - L32
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient p - L33
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient q - L34
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient h - L35
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient k - L36
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient i - L37
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient tb - L38
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient tc - L39
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient qb - L40
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient qc
07Use earlier factsL41–50
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L41
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient ub - L42
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient uc - L43
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient x - L44
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient d - L45
apply distinct_odd_prime_semantic_row_equals_decoded_quotient - L46
exact hpodd - L47
exact hqodd - L48
exact hp - L49
exact hq - L50
exact hpq
08Use earlier factsL51–55
09Calculate and transport equalitiesL56–57
10Use earlier factsL58–58
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L58
exact hstored_witness_left
Original defined command ledger · 58 lines
- 0001
intro p - 0002
intro q - 0003
intro h - 0004
intro k - 0005
intro i - 0006
intro tb - 0007
intro tc - 0008
intro qb - 0009
intro qc - 0010
intro ub - 0011
intro uc - 0012
intro cb - 0013
intro cc - 0014
intro d - 0015
intro hpodd - 0016
intro hqodd - 0017
intro hp - 0018
intro hq - 0019
intro hpq - 0020
intro hi - 0021
intro hscaled - 0022
intro hdivisions - 0023
intro hrectangle - 0024
intro hdentry - 0025
have hstored : ∃ n. 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))Exact native replay line
have hstored : exists n. ((((exists ff_h_outer_sum_bridge_stored_entry. ff_h_outer_sum_bridge_stored_entry + S (n) = S ((S (i)) * cc)) /\ exists ff_q_outer_sum_bridge_stored_entry. cb = ff_q_outer_sum_bridge_stored_entry * S ((S (i)) * cc) + (n))) /\ (exists erc_row_code_outer_sum_bridge_stored_semantics erc_row_scale_outer_sum_bridge_stored_semantics. ((forall eri_column_erc_outer_sum_bridge_stored_semantics_row. (exists eri_gap_erc_outer_sum_bridge_stored_semantics_row_bound. eri_gap_erc_outer_sum_bridge_stored_semantics_row_bound + S (eri_column_erc_outer_sum_bridge_stored_semantics_row) = k) -> exists eri_bit_erc_outer_sum_bridge_stored_semantics_row. ((((exists ff_h_eri_erc_outer_sum_bridge_stored_semantics_row_decoded. ff_h_eri_erc_outer_sum_bridge_stored_semantics_row_decoded + S (eri_bit_erc_outer_sum_bridge_stored_semantics_row) = S ((S (eri_column_erc_outer_sum_bridge_stored_semantics_row)) * erc_row_scale_outer_sum_bridge_stored_semantics)) /\ exists ff_q_eri_erc_outer_sum_bridge_stored_semantics_row_decoded. erc_row_code_outer_sum_bridge_stored_semantics = ff_q_eri_erc_outer_sum_bridge_stored_semantics_row_decoded * S ((S (eri_column_erc_outer_sum_bridge_stored_semantics_row)) * erc_row_scale_outer_sum_bridge_stored_semantics) + (eri_bit_erc_outer_sum_bridge_stored_semantics_row))) /\ (((eri_bit_erc_outer_sum_bridge_stored_semantics_row = 0 /\ ((exists eri_gap_erc_outer_sum_bridge_stored_semantics_row_choice_left. eri_gap_erc_outer_sum_bridge_stored_semantics_row_choice_left + S (q * S i) = p * S eri_column_erc_outer_sum_bridge_stored_semantics_row) /\ ~(exists eri_gap_erc_outer_sum_bridge_stored_semantics_row_choice_right. eri_gap_erc_outer_sum_bridge_stored_semantics_row_choice_right + S (p * S eri_column_erc_outer_sum_bridge_stored_semantics_row) = q * S i))) \/ (eri_bit_erc_outer_sum_bridge_stored_semantics_row = 1 /\ ((exists eri_gap_erc_outer_sum_bridge_stored_semantics_row_choice_right. eri_gap_erc_outer_sum_bridge_stored_semantics_row_choice_right + S (p * S eri_column_erc_outer_sum_bridge_stored_semantics_row) = q * S i) /\ ~(exists eri_gap_erc_outer_sum_bridge_stored_semantics_row_choice_left. eri_gap_erc_outer_sum_bridge_stored_semantics_row_choice_left + S (q * S i) = p * S eri_column_erc_outer_sum_bridge_stored_semantics_row))))))) /\ (((exists ff_u_erc_outer_sum_bridge_stored_semantics_count_sum ff_v_erc_outer_sum_bridge_stored_semantics_count_sum. ((((exists ff_h_erc_outer_sum_bridge_stored_semantics_count_sum_start. ff_h_erc_outer_sum_bridge_stored_semantics_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_outer_sum_bridge_stored_semantics_count_sum)) /\ exists ff_q_erc_outer_sum_bridge_stored_semantics_count_sum_start. ff_u_erc_outer_sum_bridge_stored_semantics_count_sum = ff_q_erc_outer_sum_bridge_stored_semantics_count_sum_start * S ((S (0)) * ff_v_erc_outer_sum_bridge_stored_semantics_count_sum) + (0))) /\ ((((exists ff_h_erc_outer_sum_bridge_stored_semantics_count_sum_terminal. ff_h_erc_outer_sum_bridge_stored_semantics_count_sum_terminal + S (n) = S ((S (k)) * ff_v_erc_outer_sum_bridge_stored_semantics_count_sum)) /\ exists ff_q_erc_outer_sum_bridge_stored_semantics_count_sum_terminal. ff_u_erc_outer_sum_bridge_stored_semantics_count_sum = ff_q_erc_outer_sum_bridge_stored_semantics_count_sum_terminal * S ((S (k)) * ff_v_erc_outer_sum_bridge_stored_semantics_count_sum) + (n))) /\ forall ff_i_erc_outer_sum_bridge_stored_semantics_count_sum. (exists ff_lt_erc_outer_sum_bridge_stored_semantics_count_sum_bound. ff_lt_erc_outer_sum_bridge_stored_semantics_count_sum_bound + S ff_i_erc_outer_sum_bridge_stored_semantics_count_sum = k) -> exists ff_a_erc_outer_sum_bridge_stored_semantics_count_sum ff_r_erc_outer_sum_bridge_stored_semantics_count_sum ff_s_erc_outer_sum_bridge_stored_semantics_count_sum. ((((exists ff_h_erc_outer_sum_bridge_stored_semantics_count_sum_summand. ff_h_erc_outer_sum_bridge_stored_semantics_count_sum_summand + S (ff_a_erc_outer_sum_bridge_stored_semantics_count_sum) = S ((S (ff_i_erc_outer_sum_bridge_stored_semantics_count_sum)) * erc_row_scale_outer_sum_bridge_stored_semantics)) /\ exists ff_q_erc_outer_sum_bridge_stored_semantics_count_sum_summand. erc_row_code_outer_sum_bridge_stored_semantics = ff_q_erc_outer_sum_bridge_stored_semantics_count_sum_summand * S ((S (ff_i_erc_outer_sum_bridge_stored_semantics_count_sum)) * erc_row_scale_outer_sum_bridge_stored_semantics) + (ff_a_erc_outer_sum_bridge_stored_semantics_count_sum))) /\ ((((exists ff_h_erc_outer_sum_bridge_stored_semantics_count_sum_partial. ff_h_erc_outer_sum_bridge_stored_semantics_count_sum_partial + S (ff_r_erc_outer_sum_bridge_stored_semantics_count_sum) = S ((S (ff_i_erc_outer_sum_bridge_stored_semantics_count_sum)) * ff_v_erc_outer_sum_bridge_stored_semantics_count_sum)) /\ exists ff_q_erc_outer_sum_bridge_stored_semantics_count_sum_partial. ff_u_erc_outer_sum_bridge_stored_semantics_count_sum = ff_q_erc_outer_sum_bridge_stored_semantics_count_sum_partial * S ((S (ff_i_erc_outer_sum_bridge_stored_semantics_count_sum)) * ff_v_erc_outer_sum_bridge_stored_semantics_count_sum) + (ff_r_erc_outer_sum_bridge_stored_semantics_count_sum))) /\ ((((exists ff_h_erc_outer_sum_bridge_stored_semantics_count_sum_successor. ff_h_erc_outer_sum_bridge_stored_semantics_count_sum_successor + S (ff_s_erc_outer_sum_bridge_stored_semantics_count_sum) = S ((S (S ff_i_erc_outer_sum_bridge_stored_semantics_count_sum)) * ff_v_erc_outer_sum_bridge_stored_semantics_count_sum)) /\ exists ff_q_erc_outer_sum_bridge_stored_semantics_count_sum_successor. ff_u_erc_outer_sum_bridge_stored_semantics_count_sum = ff_q_erc_outer_sum_bridge_stored_semantics_count_sum_successor * S ((S (S ff_i_erc_outer_sum_bridge_stored_semantics_count_sum)) * ff_v_erc_outer_sum_bridge_stored_semantics_count_sum) + (ff_s_erc_outer_sum_bridge_stored_semantics_count_sum))) /\ ff_s_erc_outer_sum_bridge_stored_semantics_count_sum = ff_r_erc_outer_sum_bridge_stored_semantics_count_sum + ff_a_erc_outer_sum_bridge_stored_semantics_count_sum)))))) /\ (forall ff_i_erc_outer_sum_bridge_stored_semantics_count_bits. (exists ff_lt_erc_outer_sum_bridge_stored_semantics_count_bits_bound. ff_lt_erc_outer_sum_bridge_stored_semantics_count_bits_bound + S ff_i_erc_outer_sum_bridge_stored_semantics_count_bits = k) -> exists ff_bit_erc_outer_sum_bridge_stored_semantics_count_bits. ((((exists ff_h_erc_outer_sum_bridge_stored_semantics_count_bits_decoded. ff_h_erc_outer_sum_bridge_stored_semantics_count_bits_decoded + S (ff_bit_erc_outer_sum_bridge_stored_semantics_count_bits) = S ((S (ff_i_erc_outer_sum_bridge_stored_semantics_count_bits)) * erc_row_scale_outer_sum_bridge_stored_semantics)) /\ exists ff_q_erc_outer_sum_bridge_stored_semantics_count_bits_decoded. erc_row_code_outer_sum_bridge_stored_semantics = ff_q_erc_outer_sum_bridge_stored_semantics_count_bits_decoded * S ((S (ff_i_erc_outer_sum_bridge_stored_semantics_count_bits)) * erc_row_scale_outer_sum_bridge_stored_semantics) + (ff_bit_erc_outer_sum_bridge_stored_semantics_count_bits))) /\ (ff_bit_erc_outer_sum_bridge_stored_semantics_count_bits = 0 \/ ff_bit_erc_outer_sum_bridge_stored_semantics_count_bits = 1)))))))) - 0026
specialize hrectangle i - 0027
apply hrectangle - 0028
exact hi - 0029
cases hstored - 0030
cases hstored_witness - 0031
have hnd : x = d - 0032
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient p - 0033
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient q - 0034
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient h - 0035
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient k - 0036
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient i - 0037
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient tb - 0038
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient tc - 0039
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient qb - 0040
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient qc - 0041
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient ub - 0042
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient uc - 0043
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient x - 0044
specialize distinct_odd_prime_semantic_row_equals_decoded_quotient d - 0045
apply distinct_odd_prime_semantic_row_equals_decoded_quotient - 0046
exact hpodd - 0047
exact hqodd - 0048
exact hp - 0049
exact hq - 0050
exact hpq - 0051
exact hi - 0052
exact hscaled - 0053
exact hdivisions - 0054
exact hstored_witness_right - 0055
exact hdentry - 0056
rewrite hnd at hstored_witness_left - 0057
rewrite hnd at hstored_witness_left - 0058
exact hstored_witness_left