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. p = 2 · h + 1 → q = 2 · k + 1 → Prime(p) → Prime(q) → ¬p = q → ∃ x. ∃ y. ∃ z. (∀ n. Lt(n,h) → ∃ m. BetaAt(x,y,n,m) ∧ (∃ i. ∃ j. (∀ u. Lt(u,k) → ∃ v. BetaAt(i,j,u,v) ∧ (v = 0 ∧ (Lt(q · S n,p · S u) ∧ ¬Lt(p · S u,q · S n)) ∨ v = 1 ∧ (Lt(p · S u,q · S n) ∧ ¬Lt(q · S n,p · S u)))) ∧ BitCount(i,j,k,m))) ∧ Sum(x,y,h,z)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
12 occurrences
In local proof propositions
10 occurrences
Exact expanded native-PA statement
forall p q h k. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_rectangle_count_prime_p frp_prime_right_rectangle_count_prime_p. p = frp_prime_left_rectangle_count_prime_p * frp_prime_right_rectangle_count_prime_p -> frp_prime_left_rectangle_count_prime_p = 1 \/ frp_prime_right_rectangle_count_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_rectangle_count_prime_q frp_prime_right_rectangle_count_prime_q. q = frp_prime_left_rectangle_count_prime_q * frp_prime_right_rectangle_count_prime_q -> frp_prime_left_rectangle_count_prime_q = 1 \/ frp_prime_right_rectangle_count_prime_q = 1)) -> ~(p = q) -> (exists cb cc total. ((forall erc_row_rectangle_count_total_prefix. (exists erc_lt_gap_rectangle_count_total_prefix_bound. erc_lt_gap_rectangle_count_total_prefix_bound + S (erc_row_rectangle_count_total_prefix) = h) -> exists erc_count_rectangle_count_total_prefix. ((((exists ff_h_erc_rectangle_count_total_prefix_decoded. ff_h_erc_rectangle_count_total_prefix_decoded + S (erc_count_rectangle_count_total_prefix) = S ((S (erc_row_rectangle_count_total_prefix)) * cc)) /\ exists ff_q_erc_rectangle_count_total_prefix_decoded. cb = ff_q_erc_rectangle_count_total_prefix_decoded * S ((S (erc_row_rectangle_count_total_prefix)) * cc) + (erc_count_rectangle_count_total_prefix))) /\ (exists erc_row_code_rectangle_count_total_prefix_witness erc_row_scale_rectangle_count_total_prefix_witness. ((forall eri_column_erc_rectangle_count_total_prefix_witness_row. (exists eri_gap_erc_rectangle_count_total_prefix_witness_row_bound. eri_gap_erc_rectangle_count_total_prefix_witness_row_bound + S (eri_column_erc_rectangle_count_total_prefix_witness_row) = k) -> exists eri_bit_erc_rectangle_count_total_prefix_witness_row. ((((exists ff_h_eri_erc_rectangle_count_total_prefix_witness_row_decoded. ff_h_eri_erc_rectangle_count_total_prefix_witness_row_decoded + S (eri_bit_erc_rectangle_count_total_prefix_witness_row) = S ((S (eri_column_erc_rectangle_count_total_prefix_witness_row)) * erc_row_scale_rectangle_count_total_prefix_witness)) /\ exists ff_q_eri_erc_rectangle_count_total_prefix_witness_row_decoded. erc_row_code_rectangle_count_total_prefix_witness = ff_q_eri_erc_rectangle_count_total_prefix_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_total_prefix_witness_row)) * erc_row_scale_rectangle_count_total_prefix_witness) + (eri_bit_erc_rectangle_count_total_prefix_witness_row))) /\ (((eri_bit_erc_rectangle_count_total_prefix_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_total_prefix) = p * S eri_column_erc_rectangle_count_total_prefix_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_total_prefix_witness_row) = q * S erc_row_rectangle_count_total_prefix))) \/ (eri_bit_erc_rectangle_count_total_prefix_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_total_prefix_witness_row) = q * S erc_row_rectangle_count_total_prefix) /\ ~(exists eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_total_prefix) = p * S eri_column_erc_rectangle_count_total_prefix_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_total_prefix_witness_count_sum ff_v_erc_rectangle_count_total_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_total_prefix_witness_count_sum_start. ff_h_erc_rectangle_count_total_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_total_prefix_witness_count_sum_start. ff_u_erc_rectangle_count_total_prefix_witness_count_sum = ff_q_erc_rectangle_count_total_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_total_prefix_witness_count_sum_terminal. ff_h_erc_rectangle_count_total_prefix_witness_count_sum_terminal + S (erc_count_rectangle_count_total_prefix) = S ((S (k)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_total_prefix_witness_count_sum_terminal. ff_u_erc_rectangle_count_total_prefix_witness_count_sum = ff_q_erc_rectangle_count_total_prefix_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum) + (erc_count_rectangle_count_total_prefix))) /\ forall ff_i_erc_rectangle_count_total_prefix_witness_count_sum. (exists ff_lt_erc_rectangle_count_total_prefix_witness_count_sum_bound. ff_lt_erc_rectangle_count_total_prefix_witness_count_sum_bound + S ff_i_erc_rectangle_count_total_prefix_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_total_prefix_witness_count_sum ff_r_erc_rectangle_count_total_prefix_witness_count_sum ff_s_erc_rectangle_count_total_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_total_prefix_witness_count_sum_summand. ff_h_erc_rectangle_count_total_prefix_witness_count_sum_summand + S (ff_a_erc_rectangle_count_total_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_total_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_total_prefix_witness)) /\ exists ff_q_erc_rectangle_count_total_prefix_witness_count_sum_summand. erc_row_code_rectangle_count_total_prefix_witness = ff_q_erc_rectangle_count_total_prefix_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_total_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_total_prefix_witness) + (ff_a_erc_rectangle_count_total_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_total_prefix_witness_count_sum_partial. ff_h_erc_rectangle_count_total_prefix_witness_count_sum_partial + S (ff_r_erc_rectangle_count_total_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_total_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_total_prefix_witness_count_sum_partial. ff_u_erc_rectangle_count_total_prefix_witness_count_sum = ff_q_erc_rectangle_count_total_prefix_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_total_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum) + (ff_r_erc_rectangle_count_total_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_total_prefix_witness_count_sum_successor. ff_h_erc_rectangle_count_total_prefix_witness_count_sum_successor + S (ff_s_erc_rectangle_count_total_prefix_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_total_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_total_prefix_witness_count_sum_successor. ff_u_erc_rectangle_count_total_prefix_witness_count_sum = ff_q_erc_rectangle_count_total_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_total_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum) + (ff_s_erc_rectangle_count_total_prefix_witness_count_sum))) /\ ff_s_erc_rectangle_count_total_prefix_witness_count_sum = ff_r_erc_rectangle_count_total_prefix_witness_count_sum + ff_a_erc_rectangle_count_total_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_total_prefix_witness_count_bits. (exists ff_lt_erc_rectangle_count_total_prefix_witness_count_bits_bound. ff_lt_erc_rectangle_count_total_prefix_witness_count_bits_bound + S ff_i_erc_rectangle_count_total_prefix_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_total_prefix_witness_count_bits. ((((exists ff_h_erc_rectangle_count_total_prefix_witness_count_bits_decoded. ff_h_erc_rectangle_count_total_prefix_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_total_prefix_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_total_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_total_prefix_witness)) /\ exists ff_q_erc_rectangle_count_total_prefix_witness_count_bits_decoded. erc_row_code_rectangle_count_total_prefix_witness = ff_q_erc_rectangle_count_total_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_total_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_total_prefix_witness) + (ff_bit_erc_rectangle_count_total_prefix_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_total_prefix_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_total_prefix_witness_count_bits = 1))))))))) /\ (exists ff_u_rectangle_count_total_sum ff_v_rectangle_count_total_sum. ((((exists ff_h_rectangle_count_total_sum_start. ff_h_rectangle_count_total_sum_start + S (0) = S ((S (0)) * ff_v_rectangle_count_total_sum)) /\ exists ff_q_rectangle_count_total_sum_start. ff_u_rectangle_count_total_sum = ff_q_rectangle_count_total_sum_start * S ((S (0)) * ff_v_rectangle_count_total_sum) + (0))) /\ ((((exists ff_h_rectangle_count_total_sum_terminal. ff_h_rectangle_count_total_sum_terminal + S (total) = S ((S (h)) * ff_v_rectangle_count_total_sum)) /\ exists ff_q_rectangle_count_total_sum_terminal. ff_u_rectangle_count_total_sum = ff_q_rectangle_count_total_sum_terminal * S ((S (h)) * ff_v_rectangle_count_total_sum) + (total))) /\ forall ff_i_rectangle_count_total_sum. (exists ff_lt_rectangle_count_total_sum_bound. ff_lt_rectangle_count_total_sum_bound + S ff_i_rectangle_count_total_sum = h) -> exists ff_a_rectangle_count_total_sum ff_r_rectangle_count_total_sum ff_s_rectangle_count_total_sum. ((((exists ff_h_rectangle_count_total_sum_summand. ff_h_rectangle_count_total_sum_summand + S (ff_a_rectangle_count_total_sum) = S ((S (ff_i_rectangle_count_total_sum)) * cc)) /\ exists ff_q_rectangle_count_total_sum_summand. cb = ff_q_rectangle_count_total_sum_summand * S ((S (ff_i_rectangle_count_total_sum)) * cc) + (ff_a_rectangle_count_total_sum))) /\ ((((exists ff_h_rectangle_count_total_sum_partial. ff_h_rectangle_count_total_sum_partial + S (ff_r_rectangle_count_total_sum) = S ((S (ff_i_rectangle_count_total_sum)) * ff_v_rectangle_count_total_sum)) /\ exists ff_q_rectangle_count_total_sum_partial. ff_u_rectangle_count_total_sum = ff_q_rectangle_count_total_sum_partial * S ((S (ff_i_rectangle_count_total_sum)) * ff_v_rectangle_count_total_sum) + (ff_r_rectangle_count_total_sum))) /\ ((((exists ff_h_rectangle_count_total_sum_successor. ff_h_rectangle_count_total_sum_successor + S (ff_s_rectangle_count_total_sum) = S ((S (S ff_i_rectangle_count_total_sum)) * ff_v_rectangle_count_total_sum)) /\ exists ff_q_rectangle_count_total_sum_successor. ff_u_rectangle_count_total_sum = ff_q_rectangle_count_total_sum_successor * S ((S (S ff_i_rectangle_count_total_sum)) * ff_v_rectangle_count_total_sum) + (ff_s_rectangle_count_total_sum))) /\ ff_s_rectangle_count_total_sum = ff_r_rectangle_count_total_sum + ff_a_rectangle_count_total_sum))))))))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 (2)
01Fix variables and assumptionsL1–9
02Establish hprefixL10–19
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct odd prime half row count prefix exists.
- L10
have hprefix : ∃ cb. ∃ cc. ∀ x. Lt(x,h) → ∃ 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))Definitions: Lt(x,h)BetaAt(cb,cc,x,y)Lt(m,k)BetaAt(z,n,m,i)Lt(q · S x,p · S m)Lt(p · S m,q · S x)BitCount(z,n,k,y)Original native command in the exact edition - L11
specialize distinct_odd_prime_half_row_count_prefix_exists p - L12
specialize distinct_odd_prime_half_row_count_prefix_exists q - L13
specialize distinct_odd_prime_half_row_count_prefix_exists h - L14
specialize distinct_odd_prime_half_row_count_prefix_exists k - L15
apply distinct_odd_prime_half_row_count_prefix_exists - L16
exact hpodd - L17
exact hqodd - L18
exact hp - L19
exact hq
03Use earlier factsL20–20
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L20
exact hpq
04Separate the logical casesL21–22
05Establish hsumL23–27
Establish this local claim before using it. It is not an additional assumption.
- L23
have hsum : ∃ total. Sum(x,x1,h,total)Definitions: Sum(x,x1,h,total)Original native command in the exact edition - L24
specialize beta_sum_exists x - L25
specialize beta_sum_exists x1 - L26
specialize beta_sum_exists h - L27
exact beta_sum_exists
06Separate the logical casesL28–28
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L28
cases hsum
07Construct an explicit witnessL29–31
08Separate the logical casesL32–32
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L32
split
Original defined command ledger · 34 lines
- 0001
intro p - 0002
intro q - 0003
intro h - 0004
intro k - 0005
intro hpodd - 0006
intro hqodd - 0007
intro hp - 0008
intro hq - 0009
intro hpq - 0010
have hprefix : ∃ cb. ∃ cc. ∀ x. Lt(x,h) → ∃ 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))Exact native replay line
have hprefix : exists cb cc. (forall erc_row_rectangle_count_full_prefix. (exists erc_lt_gap_rectangle_count_full_prefix_bound. erc_lt_gap_rectangle_count_full_prefix_bound + S (erc_row_rectangle_count_full_prefix) = h) -> exists erc_count_rectangle_count_full_prefix. ((((exists ff_h_erc_rectangle_count_full_prefix_decoded. ff_h_erc_rectangle_count_full_prefix_decoded + S (erc_count_rectangle_count_full_prefix) = S ((S (erc_row_rectangle_count_full_prefix)) * cc)) /\ exists ff_q_erc_rectangle_count_full_prefix_decoded. cb = ff_q_erc_rectangle_count_full_prefix_decoded * S ((S (erc_row_rectangle_count_full_prefix)) * cc) + (erc_count_rectangle_count_full_prefix))) /\ (exists erc_row_code_rectangle_count_full_prefix_witness erc_row_scale_rectangle_count_full_prefix_witness. ((forall eri_column_erc_rectangle_count_full_prefix_witness_row. (exists eri_gap_erc_rectangle_count_full_prefix_witness_row_bound. eri_gap_erc_rectangle_count_full_prefix_witness_row_bound + S (eri_column_erc_rectangle_count_full_prefix_witness_row) = k) -> exists eri_bit_erc_rectangle_count_full_prefix_witness_row. ((((exists ff_h_eri_erc_rectangle_count_full_prefix_witness_row_decoded. ff_h_eri_erc_rectangle_count_full_prefix_witness_row_decoded + S (eri_bit_erc_rectangle_count_full_prefix_witness_row) = S ((S (eri_column_erc_rectangle_count_full_prefix_witness_row)) * erc_row_scale_rectangle_count_full_prefix_witness)) /\ exists ff_q_eri_erc_rectangle_count_full_prefix_witness_row_decoded. erc_row_code_rectangle_count_full_prefix_witness = ff_q_eri_erc_rectangle_count_full_prefix_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_full_prefix_witness_row)) * erc_row_scale_rectangle_count_full_prefix_witness) + (eri_bit_erc_rectangle_count_full_prefix_witness_row))) /\ (((eri_bit_erc_rectangle_count_full_prefix_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_full_prefix) = p * S eri_column_erc_rectangle_count_full_prefix_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_full_prefix_witness_row) = q * S erc_row_rectangle_count_full_prefix))) \/ (eri_bit_erc_rectangle_count_full_prefix_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_full_prefix_witness_row) = q * S erc_row_rectangle_count_full_prefix) /\ ~(exists eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_full_prefix) = p * S eri_column_erc_rectangle_count_full_prefix_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_full_prefix_witness_count_sum ff_v_erc_rectangle_count_full_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_start. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_start. ff_u_erc_rectangle_count_full_prefix_witness_count_sum = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_terminal. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_terminal + S (erc_count_rectangle_count_full_prefix) = S ((S (k)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_terminal. ff_u_erc_rectangle_count_full_prefix_witness_count_sum = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum) + (erc_count_rectangle_count_full_prefix))) /\ forall ff_i_erc_rectangle_count_full_prefix_witness_count_sum. (exists ff_lt_erc_rectangle_count_full_prefix_witness_count_sum_bound. ff_lt_erc_rectangle_count_full_prefix_witness_count_sum_bound + S ff_i_erc_rectangle_count_full_prefix_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_full_prefix_witness_count_sum ff_r_erc_rectangle_count_full_prefix_witness_count_sum ff_s_erc_rectangle_count_full_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_summand. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_summand + S (ff_a_erc_rectangle_count_full_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_full_prefix_witness)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_summand. erc_row_code_rectangle_count_full_prefix_witness = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_full_prefix_witness) + (ff_a_erc_rectangle_count_full_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_partial. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_partial + S (ff_r_erc_rectangle_count_full_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_partial. ff_u_erc_rectangle_count_full_prefix_witness_count_sum = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum) + (ff_r_erc_rectangle_count_full_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_successor. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_successor + S (ff_s_erc_rectangle_count_full_prefix_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_successor. ff_u_erc_rectangle_count_full_prefix_witness_count_sum = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum) + (ff_s_erc_rectangle_count_full_prefix_witness_count_sum))) /\ ff_s_erc_rectangle_count_full_prefix_witness_count_sum = ff_r_erc_rectangle_count_full_prefix_witness_count_sum + ff_a_erc_rectangle_count_full_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_full_prefix_witness_count_bits. (exists ff_lt_erc_rectangle_count_full_prefix_witness_count_bits_bound. ff_lt_erc_rectangle_count_full_prefix_witness_count_bits_bound + S ff_i_erc_rectangle_count_full_prefix_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_full_prefix_witness_count_bits. ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_bits_decoded. ff_h_erc_rectangle_count_full_prefix_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_full_prefix_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_full_prefix_witness)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_bits_decoded. erc_row_code_rectangle_count_full_prefix_witness = ff_q_erc_rectangle_count_full_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_full_prefix_witness) + (ff_bit_erc_rectangle_count_full_prefix_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_full_prefix_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_full_prefix_witness_count_bits = 1))))))))) - 0011
specialize distinct_odd_prime_half_row_count_prefix_exists p - 0012
specialize distinct_odd_prime_half_row_count_prefix_exists q - 0013
specialize distinct_odd_prime_half_row_count_prefix_exists h - 0014
specialize distinct_odd_prime_half_row_count_prefix_exists k - 0015
apply distinct_odd_prime_half_row_count_prefix_exists - 0016
exact hpodd - 0017
exact hqodd - 0018
exact hp - 0019
exact hq - 0020
exact hpq - 0021
cases hprefix - 0022
cases hprefix_witness - 0023
have hsum : ∃ total. Sum(x,x1,h,total)Exact native replay line
have hsum : exists total. (exists ff_u_rectangle_count_total_witness_sum ff_v_rectangle_count_total_witness_sum. ((((exists ff_h_rectangle_count_total_witness_sum_start. ff_h_rectangle_count_total_witness_sum_start + S (0) = S ((S (0)) * ff_v_rectangle_count_total_witness_sum)) /\ exists ff_q_rectangle_count_total_witness_sum_start. ff_u_rectangle_count_total_witness_sum = ff_q_rectangle_count_total_witness_sum_start * S ((S (0)) * ff_v_rectangle_count_total_witness_sum) + (0))) /\ ((((exists ff_h_rectangle_count_total_witness_sum_terminal. ff_h_rectangle_count_total_witness_sum_terminal + S (total) = S ((S (h)) * ff_v_rectangle_count_total_witness_sum)) /\ exists ff_q_rectangle_count_total_witness_sum_terminal. ff_u_rectangle_count_total_witness_sum = ff_q_rectangle_count_total_witness_sum_terminal * S ((S (h)) * ff_v_rectangle_count_total_witness_sum) + (total))) /\ forall ff_i_rectangle_count_total_witness_sum. (exists ff_lt_rectangle_count_total_witness_sum_bound. ff_lt_rectangle_count_total_witness_sum_bound + S ff_i_rectangle_count_total_witness_sum = h) -> exists ff_a_rectangle_count_total_witness_sum ff_r_rectangle_count_total_witness_sum ff_s_rectangle_count_total_witness_sum. ((((exists ff_h_rectangle_count_total_witness_sum_summand. ff_h_rectangle_count_total_witness_sum_summand + S (ff_a_rectangle_count_total_witness_sum) = S ((S (ff_i_rectangle_count_total_witness_sum)) * x1)) /\ exists ff_q_rectangle_count_total_witness_sum_summand. x = ff_q_rectangle_count_total_witness_sum_summand * S ((S (ff_i_rectangle_count_total_witness_sum)) * x1) + (ff_a_rectangle_count_total_witness_sum))) /\ ((((exists ff_h_rectangle_count_total_witness_sum_partial. ff_h_rectangle_count_total_witness_sum_partial + S (ff_r_rectangle_count_total_witness_sum) = S ((S (ff_i_rectangle_count_total_witness_sum)) * ff_v_rectangle_count_total_witness_sum)) /\ exists ff_q_rectangle_count_total_witness_sum_partial. ff_u_rectangle_count_total_witness_sum = ff_q_rectangle_count_total_witness_sum_partial * S ((S (ff_i_rectangle_count_total_witness_sum)) * ff_v_rectangle_count_total_witness_sum) + (ff_r_rectangle_count_total_witness_sum))) /\ ((((exists ff_h_rectangle_count_total_witness_sum_successor. ff_h_rectangle_count_total_witness_sum_successor + S (ff_s_rectangle_count_total_witness_sum) = S ((S (S ff_i_rectangle_count_total_witness_sum)) * ff_v_rectangle_count_total_witness_sum)) /\ exists ff_q_rectangle_count_total_witness_sum_successor. ff_u_rectangle_count_total_witness_sum = ff_q_rectangle_count_total_witness_sum_successor * S ((S (S ff_i_rectangle_count_total_witness_sum)) * ff_v_rectangle_count_total_witness_sum) + (ff_s_rectangle_count_total_witness_sum))) /\ ff_s_rectangle_count_total_witness_sum = ff_r_rectangle_count_total_witness_sum + ff_a_rectangle_count_total_witness_sum)))))) - 0024
specialize beta_sum_exists x - 0025
specialize beta_sum_exists x1 - 0026
specialize beta_sum_exists h - 0027
exact beta_sum_exists - 0028
cases hsum - 0029
exists x - 0030
exists x1 - 0031
exists x2 - 0032
split - 0033
exact hprefix_witness_witness - 0034
exact hsum_witness