PA00EB · theorem

eisenstein_transposed_column_prefix_all_bits

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

Every provenance-carrying transposed column is a zero/one 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. ∀ h. ∀ bb. ∀ bc. ∀ i. ∀ z. ∀ e. ∀ k. (∀ x. Lt(x,k) → ∃ y. BetaAt(z,e,x,y) ∧ (∃ n. ∃ m. ∃ j. BetaAt(bb,bc,x,n) ∧ (∀ u. Lt(u,h) → ∃ v. BetaAt(m,j,u,v) ∧ (v = 0 ∧ (Lt(p · S x,q · S u) ∧ ¬Lt(q · S u,p · S x)) ∨ v = 1 ∧ (Lt(q · S u,p · S x) ∧ ¬Lt(p · S x,q · S u)))) ∧ BitCount(m,j,h,n) ∧ BetaAt(m,j,i,y))) → Lt(i,h) → AllBits(z,e,k)

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 PD0016 AllBits PD0017 BitCount

13 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0017 BitCount

14 occurrences

Exact expanded native-PA statement
forall p q h bb bc i z e k. (forall etc_row_index_transposed_column_semantic_prefix. (exists edt_lt_gap_transposed_column_semantic_prefix_bound. edt_lt_gap_transposed_column_semantic_prefix_bound + S (etc_row_index_transposed_column_semantic_prefix) = k) -> exists etc_bit_transposed_column_semantic_prefix. ((((exists ff_h_etc_transposed_column_semantic_prefix_decoded. ff_h_etc_transposed_column_semantic_prefix_decoded + S (etc_bit_transposed_column_semantic_prefix) = S ((S (etc_row_index_transposed_column_semantic_prefix)) * e)) /\ exists ff_q_etc_transposed_column_semantic_prefix_decoded. z = ff_q_etc_transposed_column_semantic_prefix_decoded * S ((S (etc_row_index_transposed_column_semantic_prefix)) * e) + (etc_bit_transposed_column_semantic_prefix))) /\ (exists etc_count_transposed_column_semantic_prefix_witness etc_row_code_transposed_column_semantic_prefix_witness etc_row_scale_transposed_column_semantic_prefix_witness. ((((((exists ff_h_etc_transposed_column_semantic_prefix_witness_outer_entry. ff_h_etc_transposed_column_semantic_prefix_witness_outer_entry + S (etc_count_transposed_column_semantic_prefix_witness) = S ((S (etc_row_index_transposed_column_semantic_prefix)) * bc)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_outer_entry. bb = ff_q_etc_transposed_column_semantic_prefix_witness_outer_entry * S ((S (etc_row_index_transposed_column_semantic_prefix)) * bc) + (etc_count_transposed_column_semantic_prefix_witness))) /\ (forall eri_column_etc_transposed_column_semantic_prefix_witness_row. (exists eri_gap_etc_transposed_column_semantic_prefix_witness_row_bound. eri_gap_etc_transposed_column_semantic_prefix_witness_row_bound + S (eri_column_etc_transposed_column_semantic_prefix_witness_row) = h) -> exists eri_bit_etc_transposed_column_semantic_prefix_witness_row. ((((exists ff_h_eri_etc_transposed_column_semantic_prefix_witness_row_decoded. ff_h_eri_etc_transposed_column_semantic_prefix_witness_row_decoded + S (eri_bit_etc_transposed_column_semantic_prefix_witness_row) = S ((S (eri_column_etc_transposed_column_semantic_prefix_witness_row)) * etc_row_scale_transposed_column_semantic_prefix_witness)) /\ exists ff_q_eri_etc_transposed_column_semantic_prefix_witness_row_decoded. etc_row_code_transposed_column_semantic_prefix_witness = ff_q_eri_etc_transposed_column_semantic_prefix_witness_row_decoded * S ((S (eri_column_etc_transposed_column_semantic_prefix_witness_row)) * etc_row_scale_transposed_column_semantic_prefix_witness) + (eri_bit_etc_transposed_column_semantic_prefix_witness_row))) /\ (((eri_bit_etc_transposed_column_semantic_prefix_witness_row = 0 /\ ((exists eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_left. eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_left + S (p * S etc_row_index_transposed_column_semantic_prefix) = q * S eri_column_etc_transposed_column_semantic_prefix_witness_row) /\ ~(exists eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_right. eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_semantic_prefix_witness_row) = p * S etc_row_index_transposed_column_semantic_prefix))) \/ (eri_bit_etc_transposed_column_semantic_prefix_witness_row = 1 /\ ((exists eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_right. eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_semantic_prefix_witness_row) = p * S etc_row_index_transposed_column_semantic_prefix) /\ ~(exists eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_left. eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_left + S (p * S etc_row_index_transposed_column_semantic_prefix) = q * S eri_column_etc_transposed_column_semantic_prefix_witness_row)))))))) /\ (((exists ff_u_etc_transposed_column_semantic_prefix_witness_count_relation_sum ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_start. ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_start. ff_u_etc_transposed_column_semantic_prefix_witness_count_relation_sum = ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_terminal. ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_terminal + S (etc_count_transposed_column_semantic_prefix_witness) = S ((S (h)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_terminal. ff_u_etc_transposed_column_semantic_prefix_witness_count_relation_sum = ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum) + (etc_count_transposed_column_semantic_prefix_witness))) /\ forall ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum. (exists ff_lt_etc_transposed_column_semantic_prefix_witness_count_relation_sum_bound. ff_lt_etc_transposed_column_semantic_prefix_witness_count_relation_sum_bound + S ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum = h) -> exists ff_a_etc_transposed_column_semantic_prefix_witness_count_relation_sum ff_r_etc_transposed_column_semantic_prefix_witness_count_relation_sum ff_s_etc_transposed_column_semantic_prefix_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_summand. ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_summand + S (ff_a_etc_transposed_column_semantic_prefix_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) * etc_row_scale_transposed_column_semantic_prefix_witness)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_summand. etc_row_code_transposed_column_semantic_prefix_witness = ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) * etc_row_scale_transposed_column_semantic_prefix_witness) + (ff_a_etc_transposed_column_semantic_prefix_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_partial. ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_partial + S (ff_r_etc_transposed_column_semantic_prefix_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_partial. ff_u_etc_transposed_column_semantic_prefix_witness_count_relation_sum = ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum) + (ff_r_etc_transposed_column_semantic_prefix_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_successor. ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_successor + S (ff_s_etc_transposed_column_semantic_prefix_witness_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_successor. ff_u_etc_transposed_column_semantic_prefix_witness_count_relation_sum = ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum) + (ff_s_etc_transposed_column_semantic_prefix_witness_count_relation_sum))) /\ ff_s_etc_transposed_column_semantic_prefix_witness_count_relation_sum = ff_r_etc_transposed_column_semantic_prefix_witness_count_relation_sum + ff_a_etc_transposed_column_semantic_prefix_witness_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_bits. (exists ff_lt_etc_transposed_column_semantic_prefix_witness_count_relation_bits_bound. ff_lt_etc_transposed_column_semantic_prefix_witness_count_relation_bits_bound + S ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_semantic_prefix_witness_count_relation_bits. ((((exists ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_bits_decoded. ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_semantic_prefix_witness_count_relation_bits) = S ((S (ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_bits)) * etc_row_scale_transposed_column_semantic_prefix_witness)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_bits_decoded. etc_row_code_transposed_column_semantic_prefix_witness = ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_bits)) * etc_row_scale_transposed_column_semantic_prefix_witness) + (ff_bit_etc_transposed_column_semantic_prefix_witness_count_relation_bits))) /\ (ff_bit_etc_transposed_column_semantic_prefix_witness_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_semantic_prefix_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_semantic_prefix_witness_inner_entry. ff_h_etc_transposed_column_semantic_prefix_witness_inner_entry + S (etc_bit_transposed_column_semantic_prefix) = S ((S (i)) * etc_row_scale_transposed_column_semantic_prefix_witness)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_inner_entry. etc_row_code_transposed_column_semantic_prefix_witness = ff_q_etc_transposed_column_semantic_prefix_witness_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_semantic_prefix_witness) + (etc_bit_transposed_column_semantic_prefix))))))) -> (exists edt_lt_gap_transposed_column_fixed_bound. edt_lt_gap_transposed_column_fixed_bound + S (i) = h) -> (forall ff_i_transposed_column_all_bits. (exists ff_lt_transposed_column_all_bits_bound. ff_lt_transposed_column_all_bits_bound + S ff_i_transposed_column_all_bits = k) -> exists ff_bit_transposed_column_all_bits. ((((exists ff_h_transposed_column_all_bits_decoded. ff_h_transposed_column_all_bits_decoded + S (ff_bit_transposed_column_all_bits) = S ((S (ff_i_transposed_column_all_bits)) * e)) /\ exists ff_q_transposed_column_all_bits_decoded. z = ff_q_transposed_column_all_bits_decoded * S ((S (ff_i_transposed_column_all_bits)) * e) + (ff_bit_transposed_column_all_bits))) /\ (ff_bit_transposed_column_all_bits = 0 \/ ff_bit_transposed_column_all_bits = 1)))

Proof neighborhood

Direct theorem prerequisites

PA00EA eisenstein_row_indicator_decoded_choice

Direct theorem dependents

PA00EF eisenstein_row_transposed_column_count_partition PA00F7 eisenstein_fubini_column_count_witness_retarget

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

48 script commands · 13 reading checkpoints · 2 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 (1)
eisenstein row indicator decoded choice
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 bb
  5. L5
    intro bc
  6. L6
    intro i
  7. L7
    intro z
  8. L8
    intro e
  9. L9
    intro k
  10. L10
    intro hprefix
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hi
  2. L12
    intro j
  3. L13
    intro hj
03Establish hstoredL14–17

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

  1. L14
    have hstored : ∃ d. BetaAt(z,e,j,d) ∧ (∃ x. ∃ y. ∃ n. BetaAt(bb,bc,j,x) ∧ (∀ m. Lt(m,h) → ∃ k. BetaAt(y,n,m,k) ∧ (k = 0 ∧ (Lt(p · S j,q · S m) ∧ ¬Lt(q · S m,p · S j)) ∨ k = 1 ∧ (Lt(q · S m,p · S j) ∧ ¬Lt(p · S j,q · S m)))) ∧ BitCount(y,n,h,x) ∧ BetaAt(y,n,i,d))Definitions: BetaAt(z,e,j,d)BetaAt(bb,bc,j,x)Lt(m,h)BetaAt(y,n,m,k)Lt(p · S j,q · S m)Lt(q · S m,p · S j)BitCount(y,n,h,x)BetaAt(y,n,i,d)Original native command in the exact edition
  2. L15
    specialize hprefix j
  3. L16
    apply hprefix
  4. L17
    exact hj
04Separate the logical casesL18–25

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

  1. L18
    cases hstored
  2. L19
    cases hstored_witness
  3. L20
    cases hstored_witness_right
  4. L21
    cases hstored_witness_right_witness
  5. L22
    cases hstored_witness_right_witness_witness
  6. L23
    cases hstored_witness_right_witness_witness_witness
  7. L24
    cases hstored_witness_right_witness_witness_witness_left
  8. L25
    cases hstored_witness_right_witness_witness_witness_left_left
05Establish hchoiceL26–35

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

  1. L26
    have hchoice : x = 0 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)) ∨ x = 1 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i))Definitions: Lt(p · S j,q · S i)Lt(q · S i,p · S j)Original native command in the exact edition
  2. L27
    specialize eisenstein_row_indicator_decoded_choice q
  3. L28
    specialize eisenstein_row_indicator_decoded_choice p
  4. L29
    specialize eisenstein_row_indicator_decoded_choice j
  5. L30
    specialize eisenstein_row_indicator_decoded_choice x2
  6. L31
    specialize eisenstein_row_indicator_decoded_choice x3
  7. L32
    specialize eisenstein_row_indicator_decoded_choice h
  8. L33
    specialize eisenstein_row_indicator_decoded_choice i
  9. L34
    specialize eisenstein_row_indicator_decoded_choice x
  10. L35
    apply eisenstein_row_indicator_decoded_choice
06Use earlier factsL36–38

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

  1. L36
    exact hstored_witness_right_witness_witness_witness_left_left_right
  2. L37
    exact hi
  3. L38
    exact hstored_witness_right_witness_witness_witness_right
07Construct an explicit witnessL39–39

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

  1. L39
    exists x
08Separate the logical casesL40–40

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

  1. L40
    split
09Use earlier factsL41–41

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

  1. L41
    exact hstored_witness_left
10Separate the logical casesL42–44

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

  1. L42
    cases hchoice
  2. L43
    cases hchoice_left
  3. L44
    left
11Use earlier factsL45–45

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

  1. L45
    exact hchoice_left_left
12Separate the logical casesL46–47

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

  1. L46
    cases hchoice_right
  2. L47
    right
13Use earlier factsL48–48

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

  1. L48
    exact hchoice_right_left

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro i
  7. 0007intro z
  8. 0008intro e
  9. 0009intro k
  10. 0010intro hprefix
  11. 0011intro hi
  12. 0012intro j
  13. 0013intro hj
  14. 0014have hstored : ∃ d. BetaAt(z,e,j,d) ∧ (∃ x. ∃ y. ∃ n. BetaAt(bb,bc,j,x) ∧ (∀ m. Lt(m,h) → ∃ k. BetaAt(y,n,m,k) ∧ (k = 0 ∧ (Lt(p · S j,q · S m) ∧ ¬Lt(q · S m,p · S j)) ∨ k = 1 ∧ (Lt(q · S m,p · S j) ∧ ¬Lt(p · S j,q · S m)))) ∧ BitCount(y,n,h,x) ∧ BetaAt(y,n,i,d))
    Exact native replay linehave hstored : exists d. ((((exists ff_h_transposed_column_bits_stored. ff_h_transposed_column_bits_stored + S (d) = S ((S (j)) * e)) /\ exists ff_q_transposed_column_bits_stored. z = ff_q_transposed_column_bits_stored * S ((S (j)) * e) + (d))) /\ (exists etc_count_transposed_column_bits_witness etc_row_code_transposed_column_bits_witness etc_row_scale_transposed_column_bits_witness. ((((((exists ff_h_etc_transposed_column_bits_witness_outer_entry. ff_h_etc_transposed_column_bits_witness_outer_entry + S (etc_count_transposed_column_bits_witness) = S ((S (j)) * bc)) /\ exists ff_q_etc_transposed_column_bits_witness_outer_entry. bb = ff_q_etc_transposed_column_bits_witness_outer_entry * S ((S (j)) * bc) + (etc_count_transposed_column_bits_witness))) /\ (forall eri_column_etc_transposed_column_bits_witness_row. (exists eri_gap_etc_transposed_column_bits_witness_row_bound. eri_gap_etc_transposed_column_bits_witness_row_bound + S (eri_column_etc_transposed_column_bits_witness_row) = h) -> exists eri_bit_etc_transposed_column_bits_witness_row. ((((exists ff_h_eri_etc_transposed_column_bits_witness_row_decoded. ff_h_eri_etc_transposed_column_bits_witness_row_decoded + S (eri_bit_etc_transposed_column_bits_witness_row) = S ((S (eri_column_etc_transposed_column_bits_witness_row)) * etc_row_scale_transposed_column_bits_witness)) /\ exists ff_q_eri_etc_transposed_column_bits_witness_row_decoded. etc_row_code_transposed_column_bits_witness = ff_q_eri_etc_transposed_column_bits_witness_row_decoded * S ((S (eri_column_etc_transposed_column_bits_witness_row)) * etc_row_scale_transposed_column_bits_witness) + (eri_bit_etc_transposed_column_bits_witness_row))) /\ (((eri_bit_etc_transposed_column_bits_witness_row = 0 /\ ((exists eri_gap_etc_transposed_column_bits_witness_row_choice_left. eri_gap_etc_transposed_column_bits_witness_row_choice_left + S (p * S j) = q * S eri_column_etc_transposed_column_bits_witness_row) /\ ~(exists eri_gap_etc_transposed_column_bits_witness_row_choice_right. eri_gap_etc_transposed_column_bits_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_bits_witness_row) = p * S j))) \/ (eri_bit_etc_transposed_column_bits_witness_row = 1 /\ ((exists eri_gap_etc_transposed_column_bits_witness_row_choice_right. eri_gap_etc_transposed_column_bits_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_bits_witness_row) = p * S j) /\ ~(exists eri_gap_etc_transposed_column_bits_witness_row_choice_left. eri_gap_etc_transposed_column_bits_witness_row_choice_left + S (p * S j) = q * S eri_column_etc_transposed_column_bits_witness_row)))))))) /\ (((exists ff_u_etc_transposed_column_bits_witness_count_relation_sum ff_v_etc_transposed_column_bits_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_bits_witness_count_relation_sum_start. ff_h_etc_transposed_column_bits_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_bits_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_bits_witness_count_relation_sum_start. ff_u_etc_transposed_column_bits_witness_count_relation_sum = ff_q_etc_transposed_column_bits_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_bits_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_bits_witness_count_relation_sum_terminal. ff_h_etc_transposed_column_bits_witness_count_relation_sum_terminal + S (etc_count_transposed_column_bits_witness) = S ((S (h)) * ff_v_etc_transposed_column_bits_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_bits_witness_count_relation_sum_terminal. ff_u_etc_transposed_column_bits_witness_count_relation_sum = ff_q_etc_transposed_column_bits_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_bits_witness_count_relation_sum) + (etc_count_transposed_column_bits_witness))) /\ forall ff_i_etc_transposed_column_bits_witness_count_relation_sum. (exists ff_lt_etc_transposed_column_bits_witness_count_relation_sum_bound. ff_lt_etc_transposed_column_bits_witness_count_relation_sum_bound + S ff_i_etc_transposed_column_bits_witness_count_relation_sum = h) -> exists ff_a_etc_transposed_column_bits_witness_count_relation_sum ff_r_etc_transposed_column_bits_witness_count_relation_sum ff_s_etc_transposed_column_bits_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_bits_witness_count_relation_sum_summand. ff_h_etc_transposed_column_bits_witness_count_relation_sum_summand + S (ff_a_etc_transposed_column_bits_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_bits_witness_count_relation_sum)) * etc_row_scale_transposed_column_bits_witness)) /\ exists ff_q_etc_transposed_column_bits_witness_count_relation_sum_summand. etc_row_code_transposed_column_bits_witness = ff_q_etc_transposed_column_bits_witness_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_bits_witness_count_relation_sum)) * etc_row_scale_transposed_column_bits_witness) + (ff_a_etc_transposed_column_bits_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_bits_witness_count_relation_sum_partial. ff_h_etc_transposed_column_bits_witness_count_relation_sum_partial + S (ff_r_etc_transposed_column_bits_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_bits_witness_count_relation_sum)) * ff_v_etc_transposed_column_bits_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_bits_witness_count_relation_sum_partial. ff_u_etc_transposed_column_bits_witness_count_relation_sum = ff_q_etc_transposed_column_bits_witness_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_bits_witness_count_relation_sum)) * ff_v_etc_transposed_column_bits_witness_count_relation_sum) + (ff_r_etc_transposed_column_bits_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_bits_witness_count_relation_sum_successor. ff_h_etc_transposed_column_bits_witness_count_relation_sum_successor + S (ff_s_etc_transposed_column_bits_witness_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_bits_witness_count_relation_sum)) * ff_v_etc_transposed_column_bits_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_bits_witness_count_relation_sum_successor. ff_u_etc_transposed_column_bits_witness_count_relation_sum = ff_q_etc_transposed_column_bits_witness_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_bits_witness_count_relation_sum)) * ff_v_etc_transposed_column_bits_witness_count_relation_sum) + (ff_s_etc_transposed_column_bits_witness_count_relation_sum))) /\ ff_s_etc_transposed_column_bits_witness_count_relation_sum = ff_r_etc_transposed_column_bits_witness_count_relation_sum + ff_a_etc_transposed_column_bits_witness_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_bits_witness_count_relation_bits. (exists ff_lt_etc_transposed_column_bits_witness_count_relation_bits_bound. ff_lt_etc_transposed_column_bits_witness_count_relation_bits_bound + S ff_i_etc_transposed_column_bits_witness_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_bits_witness_count_relation_bits. ((((exists ff_h_etc_transposed_column_bits_witness_count_relation_bits_decoded. ff_h_etc_transposed_column_bits_witness_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_bits_witness_count_relation_bits) = S ((S (ff_i_etc_transposed_column_bits_witness_count_relation_bits)) * etc_row_scale_transposed_column_bits_witness)) /\ exists ff_q_etc_transposed_column_bits_witness_count_relation_bits_decoded. etc_row_code_transposed_column_bits_witness = ff_q_etc_transposed_column_bits_witness_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_bits_witness_count_relation_bits)) * etc_row_scale_transposed_column_bits_witness) + (ff_bit_etc_transposed_column_bits_witness_count_relation_bits))) /\ (ff_bit_etc_transposed_column_bits_witness_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_bits_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_bits_witness_inner_entry. ff_h_etc_transposed_column_bits_witness_inner_entry + S (d) = S ((S (i)) * etc_row_scale_transposed_column_bits_witness)) /\ exists ff_q_etc_transposed_column_bits_witness_inner_entry. etc_row_code_transposed_column_bits_witness = ff_q_etc_transposed_column_bits_witness_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_bits_witness) + (d))))))
  15. 0015specialize hprefix j
  16. 0016apply hprefix
  17. 0017exact hj
  18. 0018cases hstored
  19. 0019cases hstored_witness
  20. 0020cases hstored_witness_right
  21. 0021cases hstored_witness_right_witness
  22. 0022cases hstored_witness_right_witness_witness
  23. 0023cases hstored_witness_right_witness_witness_witness
  24. 0024cases hstored_witness_right_witness_witness_witness_left
  25. 0025cases hstored_witness_right_witness_witness_witness_left_left
  26. 0026have hchoice : x = 0 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)) ∨ x = 1 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i))
    Exact native replay linehave hchoice : ((x = 0 /\ ((exists eri_gap_transposed_column_bits_choice_left. eri_gap_transposed_column_bits_choice_left + S (p * S j) = q * S i) /\ ~(exists eri_gap_transposed_column_bits_choice_right. eri_gap_transposed_column_bits_choice_right + S (q * S i) = p * S j))) \/ (x = 1 /\ ((exists eri_gap_transposed_column_bits_choice_right. eri_gap_transposed_column_bits_choice_right + S (q * S i) = p * S j) /\ ~(exists eri_gap_transposed_column_bits_choice_left. eri_gap_transposed_column_bits_choice_left + S (p * S j) = q * S i))))
  27. 0027specialize eisenstein_row_indicator_decoded_choice q
  28. 0028specialize eisenstein_row_indicator_decoded_choice p
  29. 0029specialize eisenstein_row_indicator_decoded_choice j
  30. 0030specialize eisenstein_row_indicator_decoded_choice x2
  31. 0031specialize eisenstein_row_indicator_decoded_choice x3
  32. 0032specialize eisenstein_row_indicator_decoded_choice h
  33. 0033specialize eisenstein_row_indicator_decoded_choice i
  34. 0034specialize eisenstein_row_indicator_decoded_choice x
  35. 0035apply eisenstein_row_indicator_decoded_choice
  36. 0036exact hstored_witness_right_witness_witness_witness_left_left_right
  37. 0037exact hi
  38. 0038exact hstored_witness_right_witness_witness_witness_right
  39. 0039exists x
  40. 0040split
  41. 0041exact hstored_witness_left
  42. 0042cases hchoice
  43. 0043cases hchoice_left
  44. 0044left
  45. 0045exact hchoice_left_left
  46. 0046cases hchoice_right
  47. 0047right
  48. 0048exact hchoice_right_left