PA00DJ · theorem

eisenstein_rectangle_row_count_prefix_exists

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

Every finite family of semantic row counts has an outer beta prefix.

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

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

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0017 BitCount

17 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0017 BitCount

33 occurrences

Exact expanded native-PA statement
forall p q k l. (forall erc_row_rectangle_count_exists_all. (exists erc_lt_gap_rectangle_count_exists_all_bound. erc_lt_gap_rectangle_count_exists_all_bound + S (erc_row_rectangle_count_exists_all) = l) -> exists erc_count_rectangle_count_exists_all. (exists erc_row_code_rectangle_count_exists_all_witness erc_row_scale_rectangle_count_exists_all_witness. ((forall eri_column_erc_rectangle_count_exists_all_witness_row. (exists eri_gap_erc_rectangle_count_exists_all_witness_row_bound. eri_gap_erc_rectangle_count_exists_all_witness_row_bound + S (eri_column_erc_rectangle_count_exists_all_witness_row) = k) -> exists eri_bit_erc_rectangle_count_exists_all_witness_row. ((((exists ff_h_eri_erc_rectangle_count_exists_all_witness_row_decoded. ff_h_eri_erc_rectangle_count_exists_all_witness_row_decoded + S (eri_bit_erc_rectangle_count_exists_all_witness_row) = S ((S (eri_column_erc_rectangle_count_exists_all_witness_row)) * erc_row_scale_rectangle_count_exists_all_witness)) /\ exists ff_q_eri_erc_rectangle_count_exists_all_witness_row_decoded. erc_row_code_rectangle_count_exists_all_witness = ff_q_eri_erc_rectangle_count_exists_all_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_exists_all_witness_row)) * erc_row_scale_rectangle_count_exists_all_witness) + (eri_bit_erc_rectangle_count_exists_all_witness_row))) /\ (((eri_bit_erc_rectangle_count_exists_all_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_exists_all_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_all_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_all) = p * S eri_column_erc_rectangle_count_exists_all_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_exists_all_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_all_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_all_witness_row) = q * S erc_row_rectangle_count_exists_all))) \/ (eri_bit_erc_rectangle_count_exists_all_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_exists_all_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_all_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_all_witness_row) = q * S erc_row_rectangle_count_exists_all) /\ ~(exists eri_gap_erc_rectangle_count_exists_all_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_all_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_all) = p * S eri_column_erc_rectangle_count_exists_all_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_exists_all_witness_count_sum ff_v_erc_rectangle_count_exists_all_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_all_witness_count_sum_start. ff_h_erc_rectangle_count_exists_all_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_all_witness_count_sum_start. ff_u_erc_rectangle_count_exists_all_witness_count_sum = ff_q_erc_rectangle_count_exists_all_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_exists_all_witness_count_sum_terminal. ff_h_erc_rectangle_count_exists_all_witness_count_sum_terminal + S (erc_count_rectangle_count_exists_all) = S ((S (k)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_all_witness_count_sum_terminal. ff_u_erc_rectangle_count_exists_all_witness_count_sum = ff_q_erc_rectangle_count_exists_all_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum) + (erc_count_rectangle_count_exists_all))) /\ forall ff_i_erc_rectangle_count_exists_all_witness_count_sum. (exists ff_lt_erc_rectangle_count_exists_all_witness_count_sum_bound. ff_lt_erc_rectangle_count_exists_all_witness_count_sum_bound + S ff_i_erc_rectangle_count_exists_all_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_exists_all_witness_count_sum ff_r_erc_rectangle_count_exists_all_witness_count_sum ff_s_erc_rectangle_count_exists_all_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_all_witness_count_sum_summand. ff_h_erc_rectangle_count_exists_all_witness_count_sum_summand + S (ff_a_erc_rectangle_count_exists_all_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_all_witness_count_sum)) * erc_row_scale_rectangle_count_exists_all_witness)) /\ exists ff_q_erc_rectangle_count_exists_all_witness_count_sum_summand. erc_row_code_rectangle_count_exists_all_witness = ff_q_erc_rectangle_count_exists_all_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_exists_all_witness_count_sum)) * erc_row_scale_rectangle_count_exists_all_witness) + (ff_a_erc_rectangle_count_exists_all_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_all_witness_count_sum_partial. ff_h_erc_rectangle_count_exists_all_witness_count_sum_partial + S (ff_r_erc_rectangle_count_exists_all_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_all_witness_count_sum)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_all_witness_count_sum_partial. ff_u_erc_rectangle_count_exists_all_witness_count_sum = ff_q_erc_rectangle_count_exists_all_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_exists_all_witness_count_sum)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum) + (ff_r_erc_rectangle_count_exists_all_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_all_witness_count_sum_successor. ff_h_erc_rectangle_count_exists_all_witness_count_sum_successor + S (ff_s_erc_rectangle_count_exists_all_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_exists_all_witness_count_sum)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_all_witness_count_sum_successor. ff_u_erc_rectangle_count_exists_all_witness_count_sum = ff_q_erc_rectangle_count_exists_all_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_exists_all_witness_count_sum)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum) + (ff_s_erc_rectangle_count_exists_all_witness_count_sum))) /\ ff_s_erc_rectangle_count_exists_all_witness_count_sum = ff_r_erc_rectangle_count_exists_all_witness_count_sum + ff_a_erc_rectangle_count_exists_all_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_exists_all_witness_count_bits. (exists ff_lt_erc_rectangle_count_exists_all_witness_count_bits_bound. ff_lt_erc_rectangle_count_exists_all_witness_count_bits_bound + S ff_i_erc_rectangle_count_exists_all_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_exists_all_witness_count_bits. ((((exists ff_h_erc_rectangle_count_exists_all_witness_count_bits_decoded. ff_h_erc_rectangle_count_exists_all_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_exists_all_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_exists_all_witness_count_bits)) * erc_row_scale_rectangle_count_exists_all_witness)) /\ exists ff_q_erc_rectangle_count_exists_all_witness_count_bits_decoded. erc_row_code_rectangle_count_exists_all_witness = ff_q_erc_rectangle_count_exists_all_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_exists_all_witness_count_bits)) * erc_row_scale_rectangle_count_exists_all_witness) + (ff_bit_erc_rectangle_count_exists_all_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_exists_all_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_exists_all_witness_count_bits = 1)))))))) -> (exists cb cc. (forall erc_row_rectangle_count_exists_result. (exists erc_lt_gap_rectangle_count_exists_result_bound. erc_lt_gap_rectangle_count_exists_result_bound + S (erc_row_rectangle_count_exists_result) = l) -> exists erc_count_rectangle_count_exists_result. ((((exists ff_h_erc_rectangle_count_exists_result_decoded. ff_h_erc_rectangle_count_exists_result_decoded + S (erc_count_rectangle_count_exists_result) = S ((S (erc_row_rectangle_count_exists_result)) * cc)) /\ exists ff_q_erc_rectangle_count_exists_result_decoded. cb = ff_q_erc_rectangle_count_exists_result_decoded * S ((S (erc_row_rectangle_count_exists_result)) * cc) + (erc_count_rectangle_count_exists_result))) /\ (exists erc_row_code_rectangle_count_exists_result_witness erc_row_scale_rectangle_count_exists_result_witness. ((forall eri_column_erc_rectangle_count_exists_result_witness_row. (exists eri_gap_erc_rectangle_count_exists_result_witness_row_bound. eri_gap_erc_rectangle_count_exists_result_witness_row_bound + S (eri_column_erc_rectangle_count_exists_result_witness_row) = k) -> exists eri_bit_erc_rectangle_count_exists_result_witness_row. ((((exists ff_h_eri_erc_rectangle_count_exists_result_witness_row_decoded. ff_h_eri_erc_rectangle_count_exists_result_witness_row_decoded + S (eri_bit_erc_rectangle_count_exists_result_witness_row) = S ((S (eri_column_erc_rectangle_count_exists_result_witness_row)) * erc_row_scale_rectangle_count_exists_result_witness)) /\ exists ff_q_eri_erc_rectangle_count_exists_result_witness_row_decoded. erc_row_code_rectangle_count_exists_result_witness = ff_q_eri_erc_rectangle_count_exists_result_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_exists_result_witness_row)) * erc_row_scale_rectangle_count_exists_result_witness) + (eri_bit_erc_rectangle_count_exists_result_witness_row))) /\ (((eri_bit_erc_rectangle_count_exists_result_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_exists_result_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_result_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_result) = p * S eri_column_erc_rectangle_count_exists_result_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_exists_result_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_result_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_result_witness_row) = q * S erc_row_rectangle_count_exists_result))) \/ (eri_bit_erc_rectangle_count_exists_result_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_exists_result_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_result_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_result_witness_row) = q * S erc_row_rectangle_count_exists_result) /\ ~(exists eri_gap_erc_rectangle_count_exists_result_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_result_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_result) = p * S eri_column_erc_rectangle_count_exists_result_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_exists_result_witness_count_sum ff_v_erc_rectangle_count_exists_result_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_result_witness_count_sum_start. ff_h_erc_rectangle_count_exists_result_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_result_witness_count_sum_start. ff_u_erc_rectangle_count_exists_result_witness_count_sum = ff_q_erc_rectangle_count_exists_result_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_exists_result_witness_count_sum_terminal. ff_h_erc_rectangle_count_exists_result_witness_count_sum_terminal + S (erc_count_rectangle_count_exists_result) = S ((S (k)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_result_witness_count_sum_terminal. ff_u_erc_rectangle_count_exists_result_witness_count_sum = ff_q_erc_rectangle_count_exists_result_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum) + (erc_count_rectangle_count_exists_result))) /\ forall ff_i_erc_rectangle_count_exists_result_witness_count_sum. (exists ff_lt_erc_rectangle_count_exists_result_witness_count_sum_bound. ff_lt_erc_rectangle_count_exists_result_witness_count_sum_bound + S ff_i_erc_rectangle_count_exists_result_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_exists_result_witness_count_sum ff_r_erc_rectangle_count_exists_result_witness_count_sum ff_s_erc_rectangle_count_exists_result_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_result_witness_count_sum_summand. ff_h_erc_rectangle_count_exists_result_witness_count_sum_summand + S (ff_a_erc_rectangle_count_exists_result_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_result_witness_count_sum)) * erc_row_scale_rectangle_count_exists_result_witness)) /\ exists ff_q_erc_rectangle_count_exists_result_witness_count_sum_summand. erc_row_code_rectangle_count_exists_result_witness = ff_q_erc_rectangle_count_exists_result_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_exists_result_witness_count_sum)) * erc_row_scale_rectangle_count_exists_result_witness) + (ff_a_erc_rectangle_count_exists_result_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_result_witness_count_sum_partial. ff_h_erc_rectangle_count_exists_result_witness_count_sum_partial + S (ff_r_erc_rectangle_count_exists_result_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_result_witness_count_sum)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_result_witness_count_sum_partial. ff_u_erc_rectangle_count_exists_result_witness_count_sum = ff_q_erc_rectangle_count_exists_result_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_exists_result_witness_count_sum)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum) + (ff_r_erc_rectangle_count_exists_result_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_result_witness_count_sum_successor. ff_h_erc_rectangle_count_exists_result_witness_count_sum_successor + S (ff_s_erc_rectangle_count_exists_result_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_exists_result_witness_count_sum)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_result_witness_count_sum_successor. ff_u_erc_rectangle_count_exists_result_witness_count_sum = ff_q_erc_rectangle_count_exists_result_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_exists_result_witness_count_sum)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum) + (ff_s_erc_rectangle_count_exists_result_witness_count_sum))) /\ ff_s_erc_rectangle_count_exists_result_witness_count_sum = ff_r_erc_rectangle_count_exists_result_witness_count_sum + ff_a_erc_rectangle_count_exists_result_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_exists_result_witness_count_bits. (exists ff_lt_erc_rectangle_count_exists_result_witness_count_bits_bound. ff_lt_erc_rectangle_count_exists_result_witness_count_bits_bound + S ff_i_erc_rectangle_count_exists_result_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_exists_result_witness_count_bits. ((((exists ff_h_erc_rectangle_count_exists_result_witness_count_bits_decoded. ff_h_erc_rectangle_count_exists_result_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_exists_result_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_exists_result_witness_count_bits)) * erc_row_scale_rectangle_count_exists_result_witness)) /\ exists ff_q_erc_rectangle_count_exists_result_witness_count_bits_decoded. erc_row_code_rectangle_count_exists_result_witness = ff_q_erc_rectangle_count_exists_result_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_exists_result_witness_count_bits)) * erc_row_scale_rectangle_count_exists_result_witness) + (ff_bit_erc_rectangle_count_exists_result_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_exists_result_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_exists_result_witness_count_bits = 1))))))))))

Proof neighborhood

Direct theorem prerequisites

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA00DI eisenstein_rectangle_row_count_prefix_extend

Direct theorem dependents

PA00DK distinct_odd_prime_half_row_count_prefix_exists_bounded

Definition-aware tactic body

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

Read the argument

Proof checkpoints

50 script commands · 12 reading checkpoints · 5 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 (5)
add eq zero rightsucc ne zerole succle refleisenstein rectangle row count prefix extend
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro k
02Induction on lL4–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction l
  2. L5
    intro hchoices
03Construct an explicit witnessL6–7

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

  1. L6
    exists 0
  2. L7
    exists 0
04Fix variables and assumptionsL8–9

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

  1. L8
    intro i
  2. L9
    intro hi
05Separate the logical casesL10–11

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

  1. L10
    exfalso
  2. L11
    cases hi
06Establish hsiL12–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L12
    have hsi : S i = 0
  2. L13
    specialize add_eq_zero_right x
  3. L14
    specialize add_eq_zero_right (S i)
  4. L15
    apply add_eq_zero_right
  5. L16
    exact hi_witness
  6. L17
    specialize succ_ne_zero i
  7. L18
    apply succ_ne_zero
  8. L19
    exact hsi
  9. L20
    intro hchoices
07Establish hprevious_choicesL21–29

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

  1. L21
    have hprevious_choices : ∀ erc_row_rectangle_count_exists_previous_choices. Lt(erc_row_rectangle_count_exists_previous_choices,l) → ∃ x. ∃ y. ∃ z. (∀ n. Lt(n,k) → ∃ m. BetaAt(y,z,n,m) ∧ (m = 0 ∧ (Lt(q · S erc_row_rectangle_count_exists_previous_choices,p · S n) ∧ ¬Lt(p · S n,q · S erc_row_rectangle_count_exists_previous_choices)) ∨ m = 1 ∧ (Lt(p · S n,q · S erc_row_rectangle_count_exists_previous_choices) ∧ ¬Lt(q · S erc_row_rectangle_count_exists_previous_choices,p · S n)))) ∧ BitCount(y,z,k,x)Definitions: Lt(erc_row_rectangle_count_exists_previous_choices,l)Lt(n,k)BetaAt(y,z,n,m)Lt(q · S erc_row_rectangle_count_exists_previous_choices,p · S n)Lt(p · S n,q · S erc_row_rectangle_count_exists_previous_choices)BitCount(y,z,k,x)Original native command in the exact edition
  2. L22
    intro i
  3. L23
    intro hi
  4. L24
    specialize hchoices i
  5. L25
    apply hchoices
  6. L26
    specialize le_succ (S i)
  7. L27
    specialize le_succ l
  8. L28
    apply le_succ
  9. L29
    exact hi
08Establish hpreviousL30–32

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

  1. L30
    have hprevious : ∃ cb. ∃ cc. ∀ x. Lt(x,l) → ∃ y. BetaAt(cb,cc,x,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,k) → ∃ i. BetaAt(z,n,m,i) ∧ (i = 0 ∧ (Lt(q · S x,p · S m) ∧ ¬Lt(p · S m,q · S x)) ∨ i = 1 ∧ (Lt(p · S m,q · S x) ∧ ¬Lt(q · S x,p · S m)))) ∧ BitCount(z,n,k,y))Definitions: Lt(x,l)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
  2. L31
    apply IH
  3. L32
    exact hprevious_choices
09Separate the logical casesL33–34

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

  1. L33
    cases hprevious
  2. L34
    cases hprevious_witness
10Establish hlastL35–39

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

  1. L35
    have hlast : ∃ n. ∃ x. ∃ y. (∀ z. Lt(z,k) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(q · S l,p · S z) ∧ ¬Lt(p · S z,q · S l)) ∨ m = 1 ∧ (Lt(p · S z,q · S l) ∧ ¬Lt(q · S l,p · S z)))) ∧ BitCount(x,y,k,n)Definitions: Lt(z,k)BetaAt(x,y,z,m)Lt(q · S l,p · S z)Lt(p · S z,q · S l)BitCount(x,y,k,n)Original native command in the exact edition
  2. L36
    specialize hchoices l
  3. L37
    apply hchoices
  4. L38
    specialize le_refl (S l)
  5. L39
    exact le_refl
11Establish hnextL40–49

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

  1. L40
    have hnext : ∃ cb. ∃ cc. ∀ x. Lt(x,S l) → ∃ y. BetaAt(cb,cc,x,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,k) → ∃ i. BetaAt(z,n,m,i) ∧ (i = 0 ∧ (Lt(q · S x,p · S m) ∧ ¬Lt(p · S m,q · S x)) ∨ i = 1 ∧ (Lt(p · S m,q · S x) ∧ ¬Lt(q · S x,p · S m)))) ∧ BitCount(z,n,k,y))Definitions: Lt(x,S l)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
  2. L41
    specialize eisenstein_rectangle_row_count_prefix_extend p
  3. L42
    specialize eisenstein_rectangle_row_count_prefix_extend q
  4. L43
    specialize eisenstein_rectangle_row_count_prefix_extend k
  5. L44
    specialize eisenstein_rectangle_row_count_prefix_extend x
  6. L45
    specialize eisenstein_rectangle_row_count_prefix_extend x1
  7. L46
    specialize eisenstein_rectangle_row_count_prefix_extend l
  8. L47
    apply eisenstein_rectangle_row_count_prefix_extend
  9. L48
    exact hprevious_witness_witness
  10. L49
    exact hlast
12Use earlier factsL50–50

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

  1. L50
    exact hnext

Library-wide reading audit

Original defined command ledger · 50 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro k
  4. 0004induction l
  5. 0005intro hchoices
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro i
  9. 0009intro hi
  10. 0010exfalso
  11. 0011cases hi
  12. 0012have hsi : S i = 0
  13. 0013specialize add_eq_zero_right x
  14. 0014specialize add_eq_zero_right (S i)
  15. 0015apply add_eq_zero_right
  16. 0016exact hi_witness
  17. 0017specialize succ_ne_zero i
  18. 0018apply succ_ne_zero
  19. 0019exact hsi
  20. 0020intro hchoices
  21. 0021have hprevious_choices : ∀ erc_row_rectangle_count_exists_previous_choices. Lt(erc_row_rectangle_count_exists_previous_choices,l) → ∃ x. ∃ y. ∃ z. (∀ n. Lt(n,k) → ∃ m. BetaAt(y,z,n,m) ∧ (m = 0 ∧ (Lt(q · S erc_row_rectangle_count_exists_previous_choices,p · S n) ∧ ¬Lt(p · S n,q · S erc_row_rectangle_count_exists_previous_choices)) ∨ m = 1 ∧ (Lt(p · S n,q · S erc_row_rectangle_count_exists_previous_choices) ∧ ¬Lt(q · S erc_row_rectangle_count_exists_previous_choices,p · S n)))) ∧ BitCount(y,z,k,x)
    Exact native replay linehave hprevious_choices : forall erc_row_rectangle_count_exists_previous_choices. (exists erc_lt_gap_rectangle_count_exists_previous_choices_bound. erc_lt_gap_rectangle_count_exists_previous_choices_bound + S (erc_row_rectangle_count_exists_previous_choices) = l) -> exists erc_count_rectangle_count_exists_previous_choices. (exists erc_row_code_rectangle_count_exists_previous_choices_witness erc_row_scale_rectangle_count_exists_previous_choices_witness. ((forall eri_column_erc_rectangle_count_exists_previous_choices_witness_row. (exists eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_bound. eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_bound + S (eri_column_erc_rectangle_count_exists_previous_choices_witness_row) = k) -> exists eri_bit_erc_rectangle_count_exists_previous_choices_witness_row. ((((exists ff_h_eri_erc_rectangle_count_exists_previous_choices_witness_row_decoded. ff_h_eri_erc_rectangle_count_exists_previous_choices_witness_row_decoded + S (eri_bit_erc_rectangle_count_exists_previous_choices_witness_row) = S ((S (eri_column_erc_rectangle_count_exists_previous_choices_witness_row)) * erc_row_scale_rectangle_count_exists_previous_choices_witness)) /\ exists ff_q_eri_erc_rectangle_count_exists_previous_choices_witness_row_decoded. erc_row_code_rectangle_count_exists_previous_choices_witness = ff_q_eri_erc_rectangle_count_exists_previous_choices_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_exists_previous_choices_witness_row)) * erc_row_scale_rectangle_count_exists_previous_choices_witness) + (eri_bit_erc_rectangle_count_exists_previous_choices_witness_row))) /\ (((eri_bit_erc_rectangle_count_exists_previous_choices_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_previous_choices) = p * S eri_column_erc_rectangle_count_exists_previous_choices_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_previous_choices_witness_row) = q * S erc_row_rectangle_count_exists_previous_choices))) \/ (eri_bit_erc_rectangle_count_exists_previous_choices_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_previous_choices_witness_row) = q * S erc_row_rectangle_count_exists_previous_choices) /\ ~(exists eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_previous_choices) = p * S eri_column_erc_rectangle_count_exists_previous_choices_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_exists_previous_choices_witness_count_sum ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_start. ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_start. ff_u_erc_rectangle_count_exists_previous_choices_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_terminal. ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_terminal + S (erc_count_rectangle_count_exists_previous_choices) = S ((S (k)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_terminal. ff_u_erc_rectangle_count_exists_previous_choices_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum) + (erc_count_rectangle_count_exists_previous_choices))) /\ forall ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum. (exists ff_lt_erc_rectangle_count_exists_previous_choices_witness_count_sum_bound. ff_lt_erc_rectangle_count_exists_previous_choices_witness_count_sum_bound + S ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_exists_previous_choices_witness_count_sum ff_r_erc_rectangle_count_exists_previous_choices_witness_count_sum ff_s_erc_rectangle_count_exists_previous_choices_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_summand. ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_summand + S (ff_a_erc_rectangle_count_exists_previous_choices_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum)) * erc_row_scale_rectangle_count_exists_previous_choices_witness)) /\ exists ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_summand. erc_row_code_rectangle_count_exists_previous_choices_witness = ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum)) * erc_row_scale_rectangle_count_exists_previous_choices_witness) + (ff_a_erc_rectangle_count_exists_previous_choices_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_partial. ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_partial + S (ff_r_erc_rectangle_count_exists_previous_choices_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_partial. ff_u_erc_rectangle_count_exists_previous_choices_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum) + (ff_r_erc_rectangle_count_exists_previous_choices_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_successor. ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_successor + S (ff_s_erc_rectangle_count_exists_previous_choices_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_successor. ff_u_erc_rectangle_count_exists_previous_choices_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum) + (ff_s_erc_rectangle_count_exists_previous_choices_witness_count_sum))) /\ ff_s_erc_rectangle_count_exists_previous_choices_witness_count_sum = ff_r_erc_rectangle_count_exists_previous_choices_witness_count_sum + ff_a_erc_rectangle_count_exists_previous_choices_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_exists_previous_choices_witness_count_bits. (exists ff_lt_erc_rectangle_count_exists_previous_choices_witness_count_bits_bound. ff_lt_erc_rectangle_count_exists_previous_choices_witness_count_bits_bound + S ff_i_erc_rectangle_count_exists_previous_choices_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_exists_previous_choices_witness_count_bits. ((((exists ff_h_erc_rectangle_count_exists_previous_choices_witness_count_bits_decoded. ff_h_erc_rectangle_count_exists_previous_choices_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_exists_previous_choices_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_exists_previous_choices_witness_count_bits)) * erc_row_scale_rectangle_count_exists_previous_choices_witness)) /\ exists ff_q_erc_rectangle_count_exists_previous_choices_witness_count_bits_decoded. erc_row_code_rectangle_count_exists_previous_choices_witness = ff_q_erc_rectangle_count_exists_previous_choices_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_exists_previous_choices_witness_count_bits)) * erc_row_scale_rectangle_count_exists_previous_choices_witness) + (ff_bit_erc_rectangle_count_exists_previous_choices_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_exists_previous_choices_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_exists_previous_choices_witness_count_bits = 1)))))))
  22. 0022intro i
  23. 0023intro hi
  24. 0024specialize hchoices i
  25. 0025apply hchoices
  26. 0026specialize le_succ (S i)
  27. 0027specialize le_succ l
  28. 0028apply le_succ
  29. 0029exact hi
  30. 0030have hprevious : ∃ cb. ∃ cc. ∀ x. Lt(x,l) → ∃ y. BetaAt(cb,cc,x,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,k) → ∃ i. BetaAt(z,n,m,i) ∧ (i = 0 ∧ (Lt(q · S x,p · S m) ∧ ¬Lt(p · S m,q · S x)) ∨ i = 1 ∧ (Lt(p · S m,q · S x) ∧ ¬Lt(q · S x,p · S m)))) ∧ BitCount(z,n,k,y))
    Exact native replay linehave hprevious : exists cb cc. (forall erc_row_rectangle_count_exists_previous_prefix. (exists erc_lt_gap_rectangle_count_exists_previous_prefix_bound. erc_lt_gap_rectangle_count_exists_previous_prefix_bound + S (erc_row_rectangle_count_exists_previous_prefix) = l) -> exists erc_count_rectangle_count_exists_previous_prefix. ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_decoded. ff_h_erc_rectangle_count_exists_previous_prefix_decoded + S (erc_count_rectangle_count_exists_previous_prefix) = S ((S (erc_row_rectangle_count_exists_previous_prefix)) * cc)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_decoded. cb = ff_q_erc_rectangle_count_exists_previous_prefix_decoded * S ((S (erc_row_rectangle_count_exists_previous_prefix)) * cc) + (erc_count_rectangle_count_exists_previous_prefix))) /\ (exists erc_row_code_rectangle_count_exists_previous_prefix_witness erc_row_scale_rectangle_count_exists_previous_prefix_witness. ((forall eri_column_erc_rectangle_count_exists_previous_prefix_witness_row. (exists eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_bound. eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_bound + S (eri_column_erc_rectangle_count_exists_previous_prefix_witness_row) = k) -> exists eri_bit_erc_rectangle_count_exists_previous_prefix_witness_row. ((((exists ff_h_eri_erc_rectangle_count_exists_previous_prefix_witness_row_decoded. ff_h_eri_erc_rectangle_count_exists_previous_prefix_witness_row_decoded + S (eri_bit_erc_rectangle_count_exists_previous_prefix_witness_row) = S ((S (eri_column_erc_rectangle_count_exists_previous_prefix_witness_row)) * erc_row_scale_rectangle_count_exists_previous_prefix_witness)) /\ exists ff_q_eri_erc_rectangle_count_exists_previous_prefix_witness_row_decoded. erc_row_code_rectangle_count_exists_previous_prefix_witness = ff_q_eri_erc_rectangle_count_exists_previous_prefix_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_exists_previous_prefix_witness_row)) * erc_row_scale_rectangle_count_exists_previous_prefix_witness) + (eri_bit_erc_rectangle_count_exists_previous_prefix_witness_row))) /\ (((eri_bit_erc_rectangle_count_exists_previous_prefix_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_previous_prefix) = p * S eri_column_erc_rectangle_count_exists_previous_prefix_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_previous_prefix_witness_row) = q * S erc_row_rectangle_count_exists_previous_prefix))) \/ (eri_bit_erc_rectangle_count_exists_previous_prefix_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_previous_prefix_witness_row) = q * S erc_row_rectangle_count_exists_previous_prefix) /\ ~(exists eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_previous_prefix) = p * S eri_column_erc_rectangle_count_exists_previous_prefix_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_exists_previous_prefix_witness_count_sum ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_start. ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_start. ff_u_erc_rectangle_count_exists_previous_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_terminal. ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_terminal + S (erc_count_rectangle_count_exists_previous_prefix) = S ((S (k)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_terminal. ff_u_erc_rectangle_count_exists_previous_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum) + (erc_count_rectangle_count_exists_previous_prefix))) /\ forall ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum. (exists ff_lt_erc_rectangle_count_exists_previous_prefix_witness_count_sum_bound. ff_lt_erc_rectangle_count_exists_previous_prefix_witness_count_sum_bound + S ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_exists_previous_prefix_witness_count_sum ff_r_erc_rectangle_count_exists_previous_prefix_witness_count_sum ff_s_erc_rectangle_count_exists_previous_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_summand. ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_summand + S (ff_a_erc_rectangle_count_exists_previous_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_exists_previous_prefix_witness)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_summand. erc_row_code_rectangle_count_exists_previous_prefix_witness = ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_exists_previous_prefix_witness) + (ff_a_erc_rectangle_count_exists_previous_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_partial. ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_partial + S (ff_r_erc_rectangle_count_exists_previous_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_partial. ff_u_erc_rectangle_count_exists_previous_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum) + (ff_r_erc_rectangle_count_exists_previous_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_successor. ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_successor + S (ff_s_erc_rectangle_count_exists_previous_prefix_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_successor. ff_u_erc_rectangle_count_exists_previous_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum) + (ff_s_erc_rectangle_count_exists_previous_prefix_witness_count_sum))) /\ ff_s_erc_rectangle_count_exists_previous_prefix_witness_count_sum = ff_r_erc_rectangle_count_exists_previous_prefix_witness_count_sum + ff_a_erc_rectangle_count_exists_previous_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_bits. (exists ff_lt_erc_rectangle_count_exists_previous_prefix_witness_count_bits_bound. ff_lt_erc_rectangle_count_exists_previous_prefix_witness_count_bits_bound + S ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_exists_previous_prefix_witness_count_bits. ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_bits_decoded. ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_exists_previous_prefix_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_exists_previous_prefix_witness)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_bits_decoded. erc_row_code_rectangle_count_exists_previous_prefix_witness = ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_exists_previous_prefix_witness) + (ff_bit_erc_rectangle_count_exists_previous_prefix_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_exists_previous_prefix_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_exists_previous_prefix_witness_count_bits = 1)))))))))
  31. 0031apply IH
  32. 0032exact hprevious_choices
  33. 0033cases hprevious
  34. 0034cases hprevious_witness
  35. 0035have hlast : ∃ n. ∃ x. ∃ y. (∀ z. Lt(z,k) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(q · S l,p · S z) ∧ ¬Lt(p · S z,q · S l)) ∨ m = 1 ∧ (Lt(p · S z,q · S l) ∧ ¬Lt(q · S l,p · S z)))) ∧ BitCount(x,y,k,n)
    Exact native replay linehave hlast : exists n. (exists erc_row_code_rectangle_count_exists_last erc_row_scale_rectangle_count_exists_last. ((forall eri_column_erc_rectangle_count_exists_last_row. (exists eri_gap_erc_rectangle_count_exists_last_row_bound. eri_gap_erc_rectangle_count_exists_last_row_bound + S (eri_column_erc_rectangle_count_exists_last_row) = k) -> exists eri_bit_erc_rectangle_count_exists_last_row. ((((exists ff_h_eri_erc_rectangle_count_exists_last_row_decoded. ff_h_eri_erc_rectangle_count_exists_last_row_decoded + S (eri_bit_erc_rectangle_count_exists_last_row) = S ((S (eri_column_erc_rectangle_count_exists_last_row)) * erc_row_scale_rectangle_count_exists_last)) /\ exists ff_q_eri_erc_rectangle_count_exists_last_row_decoded. erc_row_code_rectangle_count_exists_last = ff_q_eri_erc_rectangle_count_exists_last_row_decoded * S ((S (eri_column_erc_rectangle_count_exists_last_row)) * erc_row_scale_rectangle_count_exists_last) + (eri_bit_erc_rectangle_count_exists_last_row))) /\ (((eri_bit_erc_rectangle_count_exists_last_row = 0 /\ ((exists eri_gap_erc_rectangle_count_exists_last_row_choice_left. eri_gap_erc_rectangle_count_exists_last_row_choice_left + S (q * S l) = p * S eri_column_erc_rectangle_count_exists_last_row) /\ ~(exists eri_gap_erc_rectangle_count_exists_last_row_choice_right. eri_gap_erc_rectangle_count_exists_last_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_last_row) = q * S l))) \/ (eri_bit_erc_rectangle_count_exists_last_row = 1 /\ ((exists eri_gap_erc_rectangle_count_exists_last_row_choice_right. eri_gap_erc_rectangle_count_exists_last_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_last_row) = q * S l) /\ ~(exists eri_gap_erc_rectangle_count_exists_last_row_choice_left. eri_gap_erc_rectangle_count_exists_last_row_choice_left + S (q * S l) = p * S eri_column_erc_rectangle_count_exists_last_row))))))) /\ (((exists ff_u_erc_rectangle_count_exists_last_count_sum ff_v_erc_rectangle_count_exists_last_count_sum. ((((exists ff_h_erc_rectangle_count_exists_last_count_sum_start. ff_h_erc_rectangle_count_exists_last_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_exists_last_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_last_count_sum_start. ff_u_erc_rectangle_count_exists_last_count_sum = ff_q_erc_rectangle_count_exists_last_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_exists_last_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_exists_last_count_sum_terminal. ff_h_erc_rectangle_count_exists_last_count_sum_terminal + S (n) = S ((S (k)) * ff_v_erc_rectangle_count_exists_last_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_last_count_sum_terminal. ff_u_erc_rectangle_count_exists_last_count_sum = ff_q_erc_rectangle_count_exists_last_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_exists_last_count_sum) + (n))) /\ forall ff_i_erc_rectangle_count_exists_last_count_sum. (exists ff_lt_erc_rectangle_count_exists_last_count_sum_bound. ff_lt_erc_rectangle_count_exists_last_count_sum_bound + S ff_i_erc_rectangle_count_exists_last_count_sum = k) -> exists ff_a_erc_rectangle_count_exists_last_count_sum ff_r_erc_rectangle_count_exists_last_count_sum ff_s_erc_rectangle_count_exists_last_count_sum. ((((exists ff_h_erc_rectangle_count_exists_last_count_sum_summand. ff_h_erc_rectangle_count_exists_last_count_sum_summand + S (ff_a_erc_rectangle_count_exists_last_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_last_count_sum)) * erc_row_scale_rectangle_count_exists_last)) /\ exists ff_q_erc_rectangle_count_exists_last_count_sum_summand. erc_row_code_rectangle_count_exists_last = ff_q_erc_rectangle_count_exists_last_count_sum_summand * S ((S (ff_i_erc_rectangle_count_exists_last_count_sum)) * erc_row_scale_rectangle_count_exists_last) + (ff_a_erc_rectangle_count_exists_last_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_last_count_sum_partial. ff_h_erc_rectangle_count_exists_last_count_sum_partial + S (ff_r_erc_rectangle_count_exists_last_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_last_count_sum)) * ff_v_erc_rectangle_count_exists_last_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_last_count_sum_partial. ff_u_erc_rectangle_count_exists_last_count_sum = ff_q_erc_rectangle_count_exists_last_count_sum_partial * S ((S (ff_i_erc_rectangle_count_exists_last_count_sum)) * ff_v_erc_rectangle_count_exists_last_count_sum) + (ff_r_erc_rectangle_count_exists_last_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_last_count_sum_successor. ff_h_erc_rectangle_count_exists_last_count_sum_successor + S (ff_s_erc_rectangle_count_exists_last_count_sum) = S ((S (S ff_i_erc_rectangle_count_exists_last_count_sum)) * ff_v_erc_rectangle_count_exists_last_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_last_count_sum_successor. ff_u_erc_rectangle_count_exists_last_count_sum = ff_q_erc_rectangle_count_exists_last_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_exists_last_count_sum)) * ff_v_erc_rectangle_count_exists_last_count_sum) + (ff_s_erc_rectangle_count_exists_last_count_sum))) /\ ff_s_erc_rectangle_count_exists_last_count_sum = ff_r_erc_rectangle_count_exists_last_count_sum + ff_a_erc_rectangle_count_exists_last_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_exists_last_count_bits. (exists ff_lt_erc_rectangle_count_exists_last_count_bits_bound. ff_lt_erc_rectangle_count_exists_last_count_bits_bound + S ff_i_erc_rectangle_count_exists_last_count_bits = k) -> exists ff_bit_erc_rectangle_count_exists_last_count_bits. ((((exists ff_h_erc_rectangle_count_exists_last_count_bits_decoded. ff_h_erc_rectangle_count_exists_last_count_bits_decoded + S (ff_bit_erc_rectangle_count_exists_last_count_bits) = S ((S (ff_i_erc_rectangle_count_exists_last_count_bits)) * erc_row_scale_rectangle_count_exists_last)) /\ exists ff_q_erc_rectangle_count_exists_last_count_bits_decoded. erc_row_code_rectangle_count_exists_last = ff_q_erc_rectangle_count_exists_last_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_exists_last_count_bits)) * erc_row_scale_rectangle_count_exists_last) + (ff_bit_erc_rectangle_count_exists_last_count_bits))) /\ (ff_bit_erc_rectangle_count_exists_last_count_bits = 0 \/ ff_bit_erc_rectangle_count_exists_last_count_bits = 1)))))))
  36. 0036specialize hchoices l
  37. 0037apply hchoices
  38. 0038specialize le_refl (S l)
  39. 0039exact le_refl
  40. 0040have hnext : ∃ cb. ∃ cc. ∀ x. Lt(x,S l) → ∃ y. BetaAt(cb,cc,x,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,k) → ∃ i. BetaAt(z,n,m,i) ∧ (i = 0 ∧ (Lt(q · S x,p · S m) ∧ ¬Lt(p · S m,q · S x)) ∨ i = 1 ∧ (Lt(p · S m,q · S x) ∧ ¬Lt(q · S x,p · S m)))) ∧ BitCount(z,n,k,y))
    Exact native replay linehave hnext : exists cb cc. (forall erc_row_rectangle_count_exists_successor_prefix. (exists erc_lt_gap_rectangle_count_exists_successor_prefix_bound. erc_lt_gap_rectangle_count_exists_successor_prefix_bound + S (erc_row_rectangle_count_exists_successor_prefix) = S l) -> exists erc_count_rectangle_count_exists_successor_prefix. ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_decoded. ff_h_erc_rectangle_count_exists_successor_prefix_decoded + S (erc_count_rectangle_count_exists_successor_prefix) = S ((S (erc_row_rectangle_count_exists_successor_prefix)) * cc)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_decoded. cb = ff_q_erc_rectangle_count_exists_successor_prefix_decoded * S ((S (erc_row_rectangle_count_exists_successor_prefix)) * cc) + (erc_count_rectangle_count_exists_successor_prefix))) /\ (exists erc_row_code_rectangle_count_exists_successor_prefix_witness erc_row_scale_rectangle_count_exists_successor_prefix_witness. ((forall eri_column_erc_rectangle_count_exists_successor_prefix_witness_row. (exists eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_bound. eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_bound + S (eri_column_erc_rectangle_count_exists_successor_prefix_witness_row) = k) -> exists eri_bit_erc_rectangle_count_exists_successor_prefix_witness_row. ((((exists ff_h_eri_erc_rectangle_count_exists_successor_prefix_witness_row_decoded. ff_h_eri_erc_rectangle_count_exists_successor_prefix_witness_row_decoded + S (eri_bit_erc_rectangle_count_exists_successor_prefix_witness_row) = S ((S (eri_column_erc_rectangle_count_exists_successor_prefix_witness_row)) * erc_row_scale_rectangle_count_exists_successor_prefix_witness)) /\ exists ff_q_eri_erc_rectangle_count_exists_successor_prefix_witness_row_decoded. erc_row_code_rectangle_count_exists_successor_prefix_witness = ff_q_eri_erc_rectangle_count_exists_successor_prefix_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_exists_successor_prefix_witness_row)) * erc_row_scale_rectangle_count_exists_successor_prefix_witness) + (eri_bit_erc_rectangle_count_exists_successor_prefix_witness_row))) /\ (((eri_bit_erc_rectangle_count_exists_successor_prefix_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_successor_prefix) = p * S eri_column_erc_rectangle_count_exists_successor_prefix_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_successor_prefix_witness_row) = q * S erc_row_rectangle_count_exists_successor_prefix))) \/ (eri_bit_erc_rectangle_count_exists_successor_prefix_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_successor_prefix_witness_row) = q * S erc_row_rectangle_count_exists_successor_prefix) /\ ~(exists eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_successor_prefix) = p * S eri_column_erc_rectangle_count_exists_successor_prefix_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_exists_successor_prefix_witness_count_sum ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_start. ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_start. ff_u_erc_rectangle_count_exists_successor_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_terminal. ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_terminal + S (erc_count_rectangle_count_exists_successor_prefix) = S ((S (k)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_terminal. ff_u_erc_rectangle_count_exists_successor_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum) + (erc_count_rectangle_count_exists_successor_prefix))) /\ forall ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum. (exists ff_lt_erc_rectangle_count_exists_successor_prefix_witness_count_sum_bound. ff_lt_erc_rectangle_count_exists_successor_prefix_witness_count_sum_bound + S ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_exists_successor_prefix_witness_count_sum ff_r_erc_rectangle_count_exists_successor_prefix_witness_count_sum ff_s_erc_rectangle_count_exists_successor_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_summand. ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_summand + S (ff_a_erc_rectangle_count_exists_successor_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_exists_successor_prefix_witness)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_summand. erc_row_code_rectangle_count_exists_successor_prefix_witness = ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_exists_successor_prefix_witness) + (ff_a_erc_rectangle_count_exists_successor_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_partial. ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_partial + S (ff_r_erc_rectangle_count_exists_successor_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_partial. ff_u_erc_rectangle_count_exists_successor_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum) + (ff_r_erc_rectangle_count_exists_successor_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_successor. ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_successor + S (ff_s_erc_rectangle_count_exists_successor_prefix_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_successor. ff_u_erc_rectangle_count_exists_successor_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum) + (ff_s_erc_rectangle_count_exists_successor_prefix_witness_count_sum))) /\ ff_s_erc_rectangle_count_exists_successor_prefix_witness_count_sum = ff_r_erc_rectangle_count_exists_successor_prefix_witness_count_sum + ff_a_erc_rectangle_count_exists_successor_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_bits. (exists ff_lt_erc_rectangle_count_exists_successor_prefix_witness_count_bits_bound. ff_lt_erc_rectangle_count_exists_successor_prefix_witness_count_bits_bound + S ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_exists_successor_prefix_witness_count_bits. ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_bits_decoded. ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_exists_successor_prefix_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_exists_successor_prefix_witness)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_bits_decoded. erc_row_code_rectangle_count_exists_successor_prefix_witness = ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_exists_successor_prefix_witness) + (ff_bit_erc_rectangle_count_exists_successor_prefix_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_exists_successor_prefix_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_exists_successor_prefix_witness_count_bits = 1)))))))))
  41. 0041specialize eisenstein_rectangle_row_count_prefix_extend p
  42. 0042specialize eisenstein_rectangle_row_count_prefix_extend q
  43. 0043specialize eisenstein_rectangle_row_count_prefix_extend k
  44. 0044specialize eisenstein_rectangle_row_count_prefix_extend x
  45. 0045specialize eisenstein_rectangle_row_count_prefix_extend x1
  46. 0046specialize eisenstein_rectangle_row_count_prefix_extend l
  47. 0047apply eisenstein_rectangle_row_count_prefix_extend
  48. 0048exact hprevious_witness_witness
  49. 0049exact hlast
  50. 0050exact hnext