PA00DF · theorem

distinct_odd_prime_half_row_count_exists

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

Every fixed half-rectangle row has an exact beta-coded indicator and BitCount witness.

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. p = 2 · h + 1 → q = 2 · k + 1 → Prime(p) → Prime(q) → ¬p = q → Lt(i,h) → ∃ x. ∃ y. ∃ z. (∀ n. Lt(n,k) → ∃ m. BetaAt(x,y,n,m) ∧ (m = 0 ∧ (Lt(q · S i,p · S n) ∧ ¬Lt(p · S n,q · S i)) ∨ m = 1 ∧ (Lt(p · S n,q · S i) ∧ ¬Lt(q · S i,p · S n)))) ∧ BitCount(x,y,k,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

PD0002 Lt PD0004 Prime PD0013 BetaAt PD0017 BitCount

10 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0016 AllBits PD0017 BitCount

13 occurrences

Exact expanded native-PA statement
forall p q h k i. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_row_indicator_prime_p frp_prime_right_row_indicator_prime_p. p = frp_prime_left_row_indicator_prime_p * frp_prime_right_row_indicator_prime_p -> frp_prime_left_row_indicator_prime_p = 1 \/ frp_prime_right_row_indicator_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_row_indicator_prime_q frp_prime_right_row_indicator_prime_q. q = frp_prime_left_row_indicator_prime_q * frp_prime_right_row_indicator_prime_q -> frp_prime_left_row_indicator_prime_q = 1 \/ frp_prime_right_row_indicator_prime_q = 1)) -> ~(p = q) -> (exists eri_gap_row_indicator_i_bound. eri_gap_row_indicator_i_bound + S (i) = h) -> (exists rb rc n. ((forall eri_column_row_indicator_counted_prefix. (exists eri_gap_row_indicator_counted_prefix_bound. eri_gap_row_indicator_counted_prefix_bound + S (eri_column_row_indicator_counted_prefix) = k) -> exists eri_bit_row_indicator_counted_prefix. ((((exists ff_h_eri_row_indicator_counted_prefix_decoded. ff_h_eri_row_indicator_counted_prefix_decoded + S (eri_bit_row_indicator_counted_prefix) = S ((S (eri_column_row_indicator_counted_prefix)) * rc)) /\ exists ff_q_eri_row_indicator_counted_prefix_decoded. rb = ff_q_eri_row_indicator_counted_prefix_decoded * S ((S (eri_column_row_indicator_counted_prefix)) * rc) + (eri_bit_row_indicator_counted_prefix))) /\ (((eri_bit_row_indicator_counted_prefix = 0 /\ ((exists eri_gap_row_indicator_counted_prefix_choice_left. eri_gap_row_indicator_counted_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_counted_prefix) /\ ~(exists eri_gap_row_indicator_counted_prefix_choice_right. eri_gap_row_indicator_counted_prefix_choice_right + S (p * S eri_column_row_indicator_counted_prefix) = q * S i))) \/ (eri_bit_row_indicator_counted_prefix = 1 /\ ((exists eri_gap_row_indicator_counted_prefix_choice_right. eri_gap_row_indicator_counted_prefix_choice_right + S (p * S eri_column_row_indicator_counted_prefix) = q * S i) /\ ~(exists eri_gap_row_indicator_counted_prefix_choice_left. eri_gap_row_indicator_counted_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_counted_prefix))))))) /\ (((exists ff_u_row_indicator_count_relation_sum ff_v_row_indicator_count_relation_sum. ((((exists ff_h_row_indicator_count_relation_sum_start. ff_h_row_indicator_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_row_indicator_count_relation_sum)) /\ exists ff_q_row_indicator_count_relation_sum_start. ff_u_row_indicator_count_relation_sum = ff_q_row_indicator_count_relation_sum_start * S ((S (0)) * ff_v_row_indicator_count_relation_sum) + (0))) /\ ((((exists ff_h_row_indicator_count_relation_sum_terminal. ff_h_row_indicator_count_relation_sum_terminal + S (n) = S ((S (k)) * ff_v_row_indicator_count_relation_sum)) /\ exists ff_q_row_indicator_count_relation_sum_terminal. ff_u_row_indicator_count_relation_sum = ff_q_row_indicator_count_relation_sum_terminal * S ((S (k)) * ff_v_row_indicator_count_relation_sum) + (n))) /\ forall ff_i_row_indicator_count_relation_sum. (exists ff_lt_row_indicator_count_relation_sum_bound. ff_lt_row_indicator_count_relation_sum_bound + S ff_i_row_indicator_count_relation_sum = k) -> exists ff_a_row_indicator_count_relation_sum ff_r_row_indicator_count_relation_sum ff_s_row_indicator_count_relation_sum. ((((exists ff_h_row_indicator_count_relation_sum_summand. ff_h_row_indicator_count_relation_sum_summand + S (ff_a_row_indicator_count_relation_sum) = S ((S (ff_i_row_indicator_count_relation_sum)) * rc)) /\ exists ff_q_row_indicator_count_relation_sum_summand. rb = ff_q_row_indicator_count_relation_sum_summand * S ((S (ff_i_row_indicator_count_relation_sum)) * rc) + (ff_a_row_indicator_count_relation_sum))) /\ ((((exists ff_h_row_indicator_count_relation_sum_partial. ff_h_row_indicator_count_relation_sum_partial + S (ff_r_row_indicator_count_relation_sum) = S ((S (ff_i_row_indicator_count_relation_sum)) * ff_v_row_indicator_count_relation_sum)) /\ exists ff_q_row_indicator_count_relation_sum_partial. ff_u_row_indicator_count_relation_sum = ff_q_row_indicator_count_relation_sum_partial * S ((S (ff_i_row_indicator_count_relation_sum)) * ff_v_row_indicator_count_relation_sum) + (ff_r_row_indicator_count_relation_sum))) /\ ((((exists ff_h_row_indicator_count_relation_sum_successor. ff_h_row_indicator_count_relation_sum_successor + S (ff_s_row_indicator_count_relation_sum) = S ((S (S ff_i_row_indicator_count_relation_sum)) * ff_v_row_indicator_count_relation_sum)) /\ exists ff_q_row_indicator_count_relation_sum_successor. ff_u_row_indicator_count_relation_sum = ff_q_row_indicator_count_relation_sum_successor * S ((S (S ff_i_row_indicator_count_relation_sum)) * ff_v_row_indicator_count_relation_sum) + (ff_s_row_indicator_count_relation_sum))) /\ ff_s_row_indicator_count_relation_sum = ff_r_row_indicator_count_relation_sum + ff_a_row_indicator_count_relation_sum)))))) /\ (forall ff_i_row_indicator_count_relation_bits. (exists ff_lt_row_indicator_count_relation_bits_bound. ff_lt_row_indicator_count_relation_bits_bound + S ff_i_row_indicator_count_relation_bits = k) -> exists ff_bit_row_indicator_count_relation_bits. ((((exists ff_h_row_indicator_count_relation_bits_decoded. ff_h_row_indicator_count_relation_bits_decoded + S (ff_bit_row_indicator_count_relation_bits) = S ((S (ff_i_row_indicator_count_relation_bits)) * rc)) /\ exists ff_q_row_indicator_count_relation_bits_decoded. rb = ff_q_row_indicator_count_relation_bits_decoded * S ((S (ff_i_row_indicator_count_relation_bits)) * rc) + (ff_bit_row_indicator_count_relation_bits))) /\ (ff_bit_row_indicator_count_relation_bits = 0 \/ ff_bit_row_indicator_count_relation_bits = 1)))))))

Proof neighborhood

Direct theorem prerequisites

PA00DB distinct_odd_prime_half_row_indicator_choices PA00DD eisenstein_row_indicator_prefix_exists PA00DE eisenstein_row_indicator_prefix_all_bits PA003I bit_count_exists

Direct theorem dependents

PA00DG distinct_odd_prime_half_row_count_choice

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

55 script commands · 12 reading checkpoints · 4 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 (4)
distinct odd prime half row indicator choiceseisenstein row indicator prefix existseisenstein row indicator prefix all bitsbit count exists
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro h
  4. L4
    intro k
  5. L5
    intro i
  6. L6
    intro hpodd
  7. L7
    intro hqodd
  8. L8
    intro hp
  9. L9
    intro hq
  10. L10
    intro hpq
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hi
03Establish hchoicesL12–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct odd prime half row indicator choices.

  1. L12
    have hchoices : ∀ eri_column_row_indicator_concrete_choices. Lt(eri_column_row_indicator_concrete_choices,k) → ∃ x. x = 0 ∧ (Lt(q · S i,p · S eri_column_row_indicator_concrete_choices) ∧ ¬Lt(p · S eri_column_row_indicator_concrete_choices,q · S i)) ∨ x = 1 ∧ (Lt(p · S eri_column_row_indicator_concrete_choices,q · S i) ∧ ¬Lt(q · S i,p · S eri_column_row_indicator_concrete_choices))Definitions: Lt(eri_column_row_indicator_concrete_choices,k)Lt(q · S i,p · S eri_column_row_indicator_concrete_choices)Lt(p · S eri_column_row_indicator_concrete_choices,q · S i)Original native command in the exact edition
  2. L13
    specialize distinct_odd_prime_half_row_indicator_choices p
  3. L14
    specialize distinct_odd_prime_half_row_indicator_choices q
  4. L15
    specialize distinct_odd_prime_half_row_indicator_choices h
  5. L16
    specialize distinct_odd_prime_half_row_indicator_choices k
  6. L17
    specialize distinct_odd_prime_half_row_indicator_choices i
  7. L18
    apply distinct_odd_prime_half_row_indicator_choices
  8. L19
    exact hpodd
  9. L20
    exact hqodd
  10. L21
    exact hp
04Use earlier factsL22–24

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

  1. L22
    exact hq
  2. L23
    exact hpq
  3. L24
    exact hi
05Establish hprefix_existsL25–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein row indicator prefix exists.

  1. L25
    have hprefix_exists : ∃ rb. ∃ rc. ∀ x. Lt(x,k) → ∃ y. BetaAt(rb,rc,x,y) ∧ (y = 0 ∧ (Lt(q · S i,p · S x) ∧ ¬Lt(p · S x,q · S i)) ∨ y = 1 ∧ (Lt(p · S x,q · S i) ∧ ¬Lt(q · S i,p · S x)))Definitions: Lt(x,k)BetaAt(rb,rc,x,y)Lt(q · S i,p · S x)Lt(p · S x,q · S i)Original native command in the exact edition
  2. L26
    specialize eisenstein_row_indicator_prefix_exists p
  3. L27
    specialize eisenstein_row_indicator_prefix_exists q
  4. L28
    specialize eisenstein_row_indicator_prefix_exists i
  5. L29
    specialize eisenstein_row_indicator_prefix_exists k
  6. L30
    apply eisenstein_row_indicator_prefix_exists
  7. L31
    exact hchoices
06Separate the logical casesL32–33

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

  1. L32
    cases hprefix_exists
  2. L33
    cases hprefix_exists_witness
07Establish hbitsL34–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein row indicator prefix all bits.

  1. L34
    have hbits : AllBits(x,x1,k)Definitions: AllBits(x,x1,k)Original native command in the exact edition
  2. L35
    specialize eisenstein_row_indicator_prefix_all_bits p
  3. L36
    specialize eisenstein_row_indicator_prefix_all_bits q
  4. L37
    specialize eisenstein_row_indicator_prefix_all_bits i
  5. L38
    specialize eisenstein_row_indicator_prefix_all_bits x
  6. L39
    specialize eisenstein_row_indicator_prefix_all_bits x1
  7. L40
    specialize eisenstein_row_indicator_prefix_all_bits k
  8. L41
    apply eisenstein_row_indicator_prefix_all_bits
  9. L42
    exact hprefix_exists_witness_witness
08Establish hcountL43–48

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

  1. L43
    have hcount : ∃ n. BitCount(x,x1,k,n)Definitions: BitCount(x,x1,k,n)Original native command in the exact edition
  2. L44
    specialize bit_count_exists x
  3. L45
    specialize bit_count_exists x1
  4. L46
    specialize bit_count_exists k
  5. L47
    apply bit_count_exists
  6. L48
    exact hbits
09Separate the logical casesL49–49

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

  1. L49
    cases hcount
10Construct an explicit witnessL50–52

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

  1. L50
    exists x
  2. L51
    exists x1
  3. L52
    exists x2
11Separate the logical casesL53–53

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

  1. L53
    split
12Use earlier factsL54–55

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

  1. L54
    exact hprefix_exists_witness_witness
  2. L55
    exact hcount_witness

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro i
  6. 0006intro hpodd
  7. 0007intro hqodd
  8. 0008intro hp
  9. 0009intro hq
  10. 0010intro hpq
  11. 0011intro hi
  12. 0012have hchoices : ∀ eri_column_row_indicator_concrete_choices. Lt(eri_column_row_indicator_concrete_choices,k) → ∃ x. x = 0 ∧ (Lt(q · S i,p · S eri_column_row_indicator_concrete_choices) ∧ ¬Lt(p · S eri_column_row_indicator_concrete_choices,q · S i)) ∨ x = 1 ∧ (Lt(p · S eri_column_row_indicator_concrete_choices,q · S i) ∧ ¬Lt(q · S i,p · S eri_column_row_indicator_concrete_choices))
    Exact native replay linehave hchoices : forall eri_column_row_indicator_concrete_choices. (exists eri_gap_row_indicator_concrete_choices_bound. eri_gap_row_indicator_concrete_choices_bound + S (eri_column_row_indicator_concrete_choices) = k) -> exists eri_bit_row_indicator_concrete_choices. (((eri_bit_row_indicator_concrete_choices = 0 /\ ((exists eri_gap_row_indicator_concrete_choices_choice_left. eri_gap_row_indicator_concrete_choices_choice_left + S (q * S i) = p * S eri_column_row_indicator_concrete_choices) /\ ~(exists eri_gap_row_indicator_concrete_choices_choice_right. eri_gap_row_indicator_concrete_choices_choice_right + S (p * S eri_column_row_indicator_concrete_choices) = q * S i))) \/ (eri_bit_row_indicator_concrete_choices = 1 /\ ((exists eri_gap_row_indicator_concrete_choices_choice_right. eri_gap_row_indicator_concrete_choices_choice_right + S (p * S eri_column_row_indicator_concrete_choices) = q * S i) /\ ~(exists eri_gap_row_indicator_concrete_choices_choice_left. eri_gap_row_indicator_concrete_choices_choice_left + S (q * S i) = p * S eri_column_row_indicator_concrete_choices)))))
  13. 0013specialize distinct_odd_prime_half_row_indicator_choices p
  14. 0014specialize distinct_odd_prime_half_row_indicator_choices q
  15. 0015specialize distinct_odd_prime_half_row_indicator_choices h
  16. 0016specialize distinct_odd_prime_half_row_indicator_choices k
  17. 0017specialize distinct_odd_prime_half_row_indicator_choices i
  18. 0018apply distinct_odd_prime_half_row_indicator_choices
  19. 0019exact hpodd
  20. 0020exact hqodd
  21. 0021exact hp
  22. 0022exact hq
  23. 0023exact hpq
  24. 0024exact hi
  25. 0025have hprefix_exists : ∃ rb. ∃ rc. ∀ x. Lt(x,k) → ∃ y. BetaAt(rb,rc,x,y) ∧ (y = 0 ∧ (Lt(q · S i,p · S x) ∧ ¬Lt(p · S x,q · S i)) ∨ y = 1 ∧ (Lt(p · S x,q · S i) ∧ ¬Lt(q · S i,p · S x)))
    Exact native replay linehave hprefix_exists : exists rb rc. (forall eri_column_row_indicator_concrete_prefix. (exists eri_gap_row_indicator_concrete_prefix_bound. eri_gap_row_indicator_concrete_prefix_bound + S (eri_column_row_indicator_concrete_prefix) = k) -> exists eri_bit_row_indicator_concrete_prefix. ((((exists ff_h_eri_row_indicator_concrete_prefix_decoded. ff_h_eri_row_indicator_concrete_prefix_decoded + S (eri_bit_row_indicator_concrete_prefix) = S ((S (eri_column_row_indicator_concrete_prefix)) * rc)) /\ exists ff_q_eri_row_indicator_concrete_prefix_decoded. rb = ff_q_eri_row_indicator_concrete_prefix_decoded * S ((S (eri_column_row_indicator_concrete_prefix)) * rc) + (eri_bit_row_indicator_concrete_prefix))) /\ (((eri_bit_row_indicator_concrete_prefix = 0 /\ ((exists eri_gap_row_indicator_concrete_prefix_choice_left. eri_gap_row_indicator_concrete_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_concrete_prefix) /\ ~(exists eri_gap_row_indicator_concrete_prefix_choice_right. eri_gap_row_indicator_concrete_prefix_choice_right + S (p * S eri_column_row_indicator_concrete_prefix) = q * S i))) \/ (eri_bit_row_indicator_concrete_prefix = 1 /\ ((exists eri_gap_row_indicator_concrete_prefix_choice_right. eri_gap_row_indicator_concrete_prefix_choice_right + S (p * S eri_column_row_indicator_concrete_prefix) = q * S i) /\ ~(exists eri_gap_row_indicator_concrete_prefix_choice_left. eri_gap_row_indicator_concrete_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_concrete_prefix)))))))
  26. 0026specialize eisenstein_row_indicator_prefix_exists p
  27. 0027specialize eisenstein_row_indicator_prefix_exists q
  28. 0028specialize eisenstein_row_indicator_prefix_exists i
  29. 0029specialize eisenstein_row_indicator_prefix_exists k
  30. 0030apply eisenstein_row_indicator_prefix_exists
  31. 0031exact hchoices
  32. 0032cases hprefix_exists
  33. 0033cases hprefix_exists_witness
  34. 0034have hbits : AllBits(x,x1,k)
    Exact native replay linehave hbits : forall ff_i_row_indicator_counted_witness_bits. (exists ff_lt_row_indicator_counted_witness_bits_bound. ff_lt_row_indicator_counted_witness_bits_bound + S ff_i_row_indicator_counted_witness_bits = k) -> exists ff_bit_row_indicator_counted_witness_bits. ((((exists ff_h_row_indicator_counted_witness_bits_decoded. ff_h_row_indicator_counted_witness_bits_decoded + S (ff_bit_row_indicator_counted_witness_bits) = S ((S (ff_i_row_indicator_counted_witness_bits)) * x1)) /\ exists ff_q_row_indicator_counted_witness_bits_decoded. x = ff_q_row_indicator_counted_witness_bits_decoded * S ((S (ff_i_row_indicator_counted_witness_bits)) * x1) + (ff_bit_row_indicator_counted_witness_bits))) /\ (ff_bit_row_indicator_counted_witness_bits = 0 \/ ff_bit_row_indicator_counted_witness_bits = 1))
  35. 0035specialize eisenstein_row_indicator_prefix_all_bits p
  36. 0036specialize eisenstein_row_indicator_prefix_all_bits q
  37. 0037specialize eisenstein_row_indicator_prefix_all_bits i
  38. 0038specialize eisenstein_row_indicator_prefix_all_bits x
  39. 0039specialize eisenstein_row_indicator_prefix_all_bits x1
  40. 0040specialize eisenstein_row_indicator_prefix_all_bits k
  41. 0041apply eisenstein_row_indicator_prefix_all_bits
  42. 0042exact hprefix_exists_witness_witness
  43. 0043have hcount : ∃ n. BitCount(x,x1,k,n)
    Exact native replay linehave hcount : exists n. (((exists ff_u_row_indicator_counted_witness_count_sum ff_v_row_indicator_counted_witness_count_sum. ((((exists ff_h_row_indicator_counted_witness_count_sum_start. ff_h_row_indicator_counted_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_row_indicator_counted_witness_count_sum)) /\ exists ff_q_row_indicator_counted_witness_count_sum_start. ff_u_row_indicator_counted_witness_count_sum = ff_q_row_indicator_counted_witness_count_sum_start * S ((S (0)) * ff_v_row_indicator_counted_witness_count_sum) + (0))) /\ ((((exists ff_h_row_indicator_counted_witness_count_sum_terminal. ff_h_row_indicator_counted_witness_count_sum_terminal + S (n) = S ((S (k)) * ff_v_row_indicator_counted_witness_count_sum)) /\ exists ff_q_row_indicator_counted_witness_count_sum_terminal. ff_u_row_indicator_counted_witness_count_sum = ff_q_row_indicator_counted_witness_count_sum_terminal * S ((S (k)) * ff_v_row_indicator_counted_witness_count_sum) + (n))) /\ forall ff_i_row_indicator_counted_witness_count_sum. (exists ff_lt_row_indicator_counted_witness_count_sum_bound. ff_lt_row_indicator_counted_witness_count_sum_bound + S ff_i_row_indicator_counted_witness_count_sum = k) -> exists ff_a_row_indicator_counted_witness_count_sum ff_r_row_indicator_counted_witness_count_sum ff_s_row_indicator_counted_witness_count_sum. ((((exists ff_h_row_indicator_counted_witness_count_sum_summand. ff_h_row_indicator_counted_witness_count_sum_summand + S (ff_a_row_indicator_counted_witness_count_sum) = S ((S (ff_i_row_indicator_counted_witness_count_sum)) * x1)) /\ exists ff_q_row_indicator_counted_witness_count_sum_summand. x = ff_q_row_indicator_counted_witness_count_sum_summand * S ((S (ff_i_row_indicator_counted_witness_count_sum)) * x1) + (ff_a_row_indicator_counted_witness_count_sum))) /\ ((((exists ff_h_row_indicator_counted_witness_count_sum_partial. ff_h_row_indicator_counted_witness_count_sum_partial + S (ff_r_row_indicator_counted_witness_count_sum) = S ((S (ff_i_row_indicator_counted_witness_count_sum)) * ff_v_row_indicator_counted_witness_count_sum)) /\ exists ff_q_row_indicator_counted_witness_count_sum_partial. ff_u_row_indicator_counted_witness_count_sum = ff_q_row_indicator_counted_witness_count_sum_partial * S ((S (ff_i_row_indicator_counted_witness_count_sum)) * ff_v_row_indicator_counted_witness_count_sum) + (ff_r_row_indicator_counted_witness_count_sum))) /\ ((((exists ff_h_row_indicator_counted_witness_count_sum_successor. ff_h_row_indicator_counted_witness_count_sum_successor + S (ff_s_row_indicator_counted_witness_count_sum) = S ((S (S ff_i_row_indicator_counted_witness_count_sum)) * ff_v_row_indicator_counted_witness_count_sum)) /\ exists ff_q_row_indicator_counted_witness_count_sum_successor. ff_u_row_indicator_counted_witness_count_sum = ff_q_row_indicator_counted_witness_count_sum_successor * S ((S (S ff_i_row_indicator_counted_witness_count_sum)) * ff_v_row_indicator_counted_witness_count_sum) + (ff_s_row_indicator_counted_witness_count_sum))) /\ ff_s_row_indicator_counted_witness_count_sum = ff_r_row_indicator_counted_witness_count_sum + ff_a_row_indicator_counted_witness_count_sum)))))) /\ (forall ff_i_row_indicator_counted_witness_count_bits. (exists ff_lt_row_indicator_counted_witness_count_bits_bound. ff_lt_row_indicator_counted_witness_count_bits_bound + S ff_i_row_indicator_counted_witness_count_bits = k) -> exists ff_bit_row_indicator_counted_witness_count_bits. ((((exists ff_h_row_indicator_counted_witness_count_bits_decoded. ff_h_row_indicator_counted_witness_count_bits_decoded + S (ff_bit_row_indicator_counted_witness_count_bits) = S ((S (ff_i_row_indicator_counted_witness_count_bits)) * x1)) /\ exists ff_q_row_indicator_counted_witness_count_bits_decoded. x = ff_q_row_indicator_counted_witness_count_bits_decoded * S ((S (ff_i_row_indicator_counted_witness_count_bits)) * x1) + (ff_bit_row_indicator_counted_witness_count_bits))) /\ (ff_bit_row_indicator_counted_witness_count_bits = 0 \/ ff_bit_row_indicator_counted_witness_count_bits = 1)))))
  44. 0044specialize bit_count_exists x
  45. 0045specialize bit_count_exists x1
  46. 0046specialize bit_count_exists k
  47. 0047apply bit_count_exists
  48. 0048exact hbits
  49. 0049cases hcount
  50. 0050exists x
  51. 0051exists x1
  52. 0052exists x2
  53. 0053split
  54. 0054exact hprefix_exists_witness_witness
  55. 0055exact hcount_witness