PA00E7 · theorem

eisenstein_transposed_outer_column_choices

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

A fixed bounded index has one provenance-carrying bit in every swapped row.

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

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

20 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0017 BitCount

9 occurrences

Exact expanded native-PA statement
forall p q h k bb bc i. (forall erc_row_transposed_column_outer. (exists erc_lt_gap_transposed_column_outer_bound. erc_lt_gap_transposed_column_outer_bound + S (erc_row_transposed_column_outer) = k) -> exists erc_count_transposed_column_outer. ((((exists ff_h_erc_transposed_column_outer_decoded. ff_h_erc_transposed_column_outer_decoded + S (erc_count_transposed_column_outer) = S ((S (erc_row_transposed_column_outer)) * bc)) /\ exists ff_q_erc_transposed_column_outer_decoded. bb = ff_q_erc_transposed_column_outer_decoded * S ((S (erc_row_transposed_column_outer)) * bc) + (erc_count_transposed_column_outer))) /\ (exists erc_row_code_transposed_column_outer_witness erc_row_scale_transposed_column_outer_witness. ((forall eri_column_erc_transposed_column_outer_witness_row. (exists eri_gap_erc_transposed_column_outer_witness_row_bound. eri_gap_erc_transposed_column_outer_witness_row_bound + S (eri_column_erc_transposed_column_outer_witness_row) = h) -> exists eri_bit_erc_transposed_column_outer_witness_row. ((((exists ff_h_eri_erc_transposed_column_outer_witness_row_decoded. ff_h_eri_erc_transposed_column_outer_witness_row_decoded + S (eri_bit_erc_transposed_column_outer_witness_row) = S ((S (eri_column_erc_transposed_column_outer_witness_row)) * erc_row_scale_transposed_column_outer_witness)) /\ exists ff_q_eri_erc_transposed_column_outer_witness_row_decoded. erc_row_code_transposed_column_outer_witness = ff_q_eri_erc_transposed_column_outer_witness_row_decoded * S ((S (eri_column_erc_transposed_column_outer_witness_row)) * erc_row_scale_transposed_column_outer_witness) + (eri_bit_erc_transposed_column_outer_witness_row))) /\ (((eri_bit_erc_transposed_column_outer_witness_row = 0 /\ ((exists eri_gap_erc_transposed_column_outer_witness_row_choice_left. eri_gap_erc_transposed_column_outer_witness_row_choice_left + S (p * S erc_row_transposed_column_outer) = q * S eri_column_erc_transposed_column_outer_witness_row) /\ ~(exists eri_gap_erc_transposed_column_outer_witness_row_choice_right. eri_gap_erc_transposed_column_outer_witness_row_choice_right + S (q * S eri_column_erc_transposed_column_outer_witness_row) = p * S erc_row_transposed_column_outer))) \/ (eri_bit_erc_transposed_column_outer_witness_row = 1 /\ ((exists eri_gap_erc_transposed_column_outer_witness_row_choice_right. eri_gap_erc_transposed_column_outer_witness_row_choice_right + S (q * S eri_column_erc_transposed_column_outer_witness_row) = p * S erc_row_transposed_column_outer) /\ ~(exists eri_gap_erc_transposed_column_outer_witness_row_choice_left. eri_gap_erc_transposed_column_outer_witness_row_choice_left + S (p * S erc_row_transposed_column_outer) = q * S eri_column_erc_transposed_column_outer_witness_row))))))) /\ (((exists ff_u_erc_transposed_column_outer_witness_count_sum ff_v_erc_transposed_column_outer_witness_count_sum. ((((exists ff_h_erc_transposed_column_outer_witness_count_sum_start. ff_h_erc_transposed_column_outer_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_transposed_column_outer_witness_count_sum)) /\ exists ff_q_erc_transposed_column_outer_witness_count_sum_start. ff_u_erc_transposed_column_outer_witness_count_sum = ff_q_erc_transposed_column_outer_witness_count_sum_start * S ((S (0)) * ff_v_erc_transposed_column_outer_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_transposed_column_outer_witness_count_sum_terminal. ff_h_erc_transposed_column_outer_witness_count_sum_terminal + S (erc_count_transposed_column_outer) = S ((S (h)) * ff_v_erc_transposed_column_outer_witness_count_sum)) /\ exists ff_q_erc_transposed_column_outer_witness_count_sum_terminal. ff_u_erc_transposed_column_outer_witness_count_sum = ff_q_erc_transposed_column_outer_witness_count_sum_terminal * S ((S (h)) * ff_v_erc_transposed_column_outer_witness_count_sum) + (erc_count_transposed_column_outer))) /\ forall ff_i_erc_transposed_column_outer_witness_count_sum. (exists ff_lt_erc_transposed_column_outer_witness_count_sum_bound. ff_lt_erc_transposed_column_outer_witness_count_sum_bound + S ff_i_erc_transposed_column_outer_witness_count_sum = h) -> exists ff_a_erc_transposed_column_outer_witness_count_sum ff_r_erc_transposed_column_outer_witness_count_sum ff_s_erc_transposed_column_outer_witness_count_sum. ((((exists ff_h_erc_transposed_column_outer_witness_count_sum_summand. ff_h_erc_transposed_column_outer_witness_count_sum_summand + S (ff_a_erc_transposed_column_outer_witness_count_sum) = S ((S (ff_i_erc_transposed_column_outer_witness_count_sum)) * erc_row_scale_transposed_column_outer_witness)) /\ exists ff_q_erc_transposed_column_outer_witness_count_sum_summand. erc_row_code_transposed_column_outer_witness = ff_q_erc_transposed_column_outer_witness_count_sum_summand * S ((S (ff_i_erc_transposed_column_outer_witness_count_sum)) * erc_row_scale_transposed_column_outer_witness) + (ff_a_erc_transposed_column_outer_witness_count_sum))) /\ ((((exists ff_h_erc_transposed_column_outer_witness_count_sum_partial. ff_h_erc_transposed_column_outer_witness_count_sum_partial + S (ff_r_erc_transposed_column_outer_witness_count_sum) = S ((S (ff_i_erc_transposed_column_outer_witness_count_sum)) * ff_v_erc_transposed_column_outer_witness_count_sum)) /\ exists ff_q_erc_transposed_column_outer_witness_count_sum_partial. ff_u_erc_transposed_column_outer_witness_count_sum = ff_q_erc_transposed_column_outer_witness_count_sum_partial * S ((S (ff_i_erc_transposed_column_outer_witness_count_sum)) * ff_v_erc_transposed_column_outer_witness_count_sum) + (ff_r_erc_transposed_column_outer_witness_count_sum))) /\ ((((exists ff_h_erc_transposed_column_outer_witness_count_sum_successor. ff_h_erc_transposed_column_outer_witness_count_sum_successor + S (ff_s_erc_transposed_column_outer_witness_count_sum) = S ((S (S ff_i_erc_transposed_column_outer_witness_count_sum)) * ff_v_erc_transposed_column_outer_witness_count_sum)) /\ exists ff_q_erc_transposed_column_outer_witness_count_sum_successor. ff_u_erc_transposed_column_outer_witness_count_sum = ff_q_erc_transposed_column_outer_witness_count_sum_successor * S ((S (S ff_i_erc_transposed_column_outer_witness_count_sum)) * ff_v_erc_transposed_column_outer_witness_count_sum) + (ff_s_erc_transposed_column_outer_witness_count_sum))) /\ ff_s_erc_transposed_column_outer_witness_count_sum = ff_r_erc_transposed_column_outer_witness_count_sum + ff_a_erc_transposed_column_outer_witness_count_sum)))))) /\ (forall ff_i_erc_transposed_column_outer_witness_count_bits. (exists ff_lt_erc_transposed_column_outer_witness_count_bits_bound. ff_lt_erc_transposed_column_outer_witness_count_bits_bound + S ff_i_erc_transposed_column_outer_witness_count_bits = h) -> exists ff_bit_erc_transposed_column_outer_witness_count_bits. ((((exists ff_h_erc_transposed_column_outer_witness_count_bits_decoded. ff_h_erc_transposed_column_outer_witness_count_bits_decoded + S (ff_bit_erc_transposed_column_outer_witness_count_bits) = S ((S (ff_i_erc_transposed_column_outer_witness_count_bits)) * erc_row_scale_transposed_column_outer_witness)) /\ exists ff_q_erc_transposed_column_outer_witness_count_bits_decoded. erc_row_code_transposed_column_outer_witness = ff_q_erc_transposed_column_outer_witness_count_bits_decoded * S ((S (ff_i_erc_transposed_column_outer_witness_count_bits)) * erc_row_scale_transposed_column_outer_witness) + (ff_bit_erc_transposed_column_outer_witness_count_bits))) /\ (ff_bit_erc_transposed_column_outer_witness_count_bits = 0 \/ ff_bit_erc_transposed_column_outer_witness_count_bits = 1))))))))) -> (exists edt_lt_gap_transposed_column_fixed_bound. edt_lt_gap_transposed_column_fixed_bound + S (i) = h) -> (forall etc_row_index_transposed_column_choices. (exists edt_lt_gap_transposed_column_choices_bound. edt_lt_gap_transposed_column_choices_bound + S (etc_row_index_transposed_column_choices) = k) -> exists etc_bit_transposed_column_choices. (exists etc_count_transposed_column_choices_witness etc_row_code_transposed_column_choices_witness etc_row_scale_transposed_column_choices_witness. ((((((exists ff_h_etc_transposed_column_choices_witness_outer_entry. ff_h_etc_transposed_column_choices_witness_outer_entry + S (etc_count_transposed_column_choices_witness) = S ((S (etc_row_index_transposed_column_choices)) * bc)) /\ exists ff_q_etc_transposed_column_choices_witness_outer_entry. bb = ff_q_etc_transposed_column_choices_witness_outer_entry * S ((S (etc_row_index_transposed_column_choices)) * bc) + (etc_count_transposed_column_choices_witness))) /\ (forall eri_column_etc_transposed_column_choices_witness_row. (exists eri_gap_etc_transposed_column_choices_witness_row_bound. eri_gap_etc_transposed_column_choices_witness_row_bound + S (eri_column_etc_transposed_column_choices_witness_row) = h) -> exists eri_bit_etc_transposed_column_choices_witness_row. ((((exists ff_h_eri_etc_transposed_column_choices_witness_row_decoded. ff_h_eri_etc_transposed_column_choices_witness_row_decoded + S (eri_bit_etc_transposed_column_choices_witness_row) = S ((S (eri_column_etc_transposed_column_choices_witness_row)) * etc_row_scale_transposed_column_choices_witness)) /\ exists ff_q_eri_etc_transposed_column_choices_witness_row_decoded. etc_row_code_transposed_column_choices_witness = ff_q_eri_etc_transposed_column_choices_witness_row_decoded * S ((S (eri_column_etc_transposed_column_choices_witness_row)) * etc_row_scale_transposed_column_choices_witness) + (eri_bit_etc_transposed_column_choices_witness_row))) /\ (((eri_bit_etc_transposed_column_choices_witness_row = 0 /\ ((exists eri_gap_etc_transposed_column_choices_witness_row_choice_left. eri_gap_etc_transposed_column_choices_witness_row_choice_left + S (p * S etc_row_index_transposed_column_choices) = q * S eri_column_etc_transposed_column_choices_witness_row) /\ ~(exists eri_gap_etc_transposed_column_choices_witness_row_choice_right. eri_gap_etc_transposed_column_choices_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_choices_witness_row) = p * S etc_row_index_transposed_column_choices))) \/ (eri_bit_etc_transposed_column_choices_witness_row = 1 /\ ((exists eri_gap_etc_transposed_column_choices_witness_row_choice_right. eri_gap_etc_transposed_column_choices_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_choices_witness_row) = p * S etc_row_index_transposed_column_choices) /\ ~(exists eri_gap_etc_transposed_column_choices_witness_row_choice_left. eri_gap_etc_transposed_column_choices_witness_row_choice_left + S (p * S etc_row_index_transposed_column_choices) = q * S eri_column_etc_transposed_column_choices_witness_row)))))))) /\ (((exists ff_u_etc_transposed_column_choices_witness_count_relation_sum ff_v_etc_transposed_column_choices_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_choices_witness_count_relation_sum_start. ff_h_etc_transposed_column_choices_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_choices_witness_count_relation_sum_start. ff_u_etc_transposed_column_choices_witness_count_relation_sum = ff_q_etc_transposed_column_choices_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_choices_witness_count_relation_sum_terminal. ff_h_etc_transposed_column_choices_witness_count_relation_sum_terminal + S (etc_count_transposed_column_choices_witness) = S ((S (h)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_choices_witness_count_relation_sum_terminal. ff_u_etc_transposed_column_choices_witness_count_relation_sum = ff_q_etc_transposed_column_choices_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum) + (etc_count_transposed_column_choices_witness))) /\ forall ff_i_etc_transposed_column_choices_witness_count_relation_sum. (exists ff_lt_etc_transposed_column_choices_witness_count_relation_sum_bound. ff_lt_etc_transposed_column_choices_witness_count_relation_sum_bound + S ff_i_etc_transposed_column_choices_witness_count_relation_sum = h) -> exists ff_a_etc_transposed_column_choices_witness_count_relation_sum ff_r_etc_transposed_column_choices_witness_count_relation_sum ff_s_etc_transposed_column_choices_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_choices_witness_count_relation_sum_summand. ff_h_etc_transposed_column_choices_witness_count_relation_sum_summand + S (ff_a_etc_transposed_column_choices_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_choices_witness_count_relation_sum)) * etc_row_scale_transposed_column_choices_witness)) /\ exists ff_q_etc_transposed_column_choices_witness_count_relation_sum_summand. etc_row_code_transposed_column_choices_witness = ff_q_etc_transposed_column_choices_witness_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_choices_witness_count_relation_sum)) * etc_row_scale_transposed_column_choices_witness) + (ff_a_etc_transposed_column_choices_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_choices_witness_count_relation_sum_partial. ff_h_etc_transposed_column_choices_witness_count_relation_sum_partial + S (ff_r_etc_transposed_column_choices_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_choices_witness_count_relation_sum)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_choices_witness_count_relation_sum_partial. ff_u_etc_transposed_column_choices_witness_count_relation_sum = ff_q_etc_transposed_column_choices_witness_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_choices_witness_count_relation_sum)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum) + (ff_r_etc_transposed_column_choices_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_choices_witness_count_relation_sum_successor. ff_h_etc_transposed_column_choices_witness_count_relation_sum_successor + S (ff_s_etc_transposed_column_choices_witness_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_choices_witness_count_relation_sum)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_choices_witness_count_relation_sum_successor. ff_u_etc_transposed_column_choices_witness_count_relation_sum = ff_q_etc_transposed_column_choices_witness_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_choices_witness_count_relation_sum)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum) + (ff_s_etc_transposed_column_choices_witness_count_relation_sum))) /\ ff_s_etc_transposed_column_choices_witness_count_relation_sum = ff_r_etc_transposed_column_choices_witness_count_relation_sum + ff_a_etc_transposed_column_choices_witness_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_choices_witness_count_relation_bits. (exists ff_lt_etc_transposed_column_choices_witness_count_relation_bits_bound. ff_lt_etc_transposed_column_choices_witness_count_relation_bits_bound + S ff_i_etc_transposed_column_choices_witness_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_choices_witness_count_relation_bits. ((((exists ff_h_etc_transposed_column_choices_witness_count_relation_bits_decoded. ff_h_etc_transposed_column_choices_witness_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_choices_witness_count_relation_bits) = S ((S (ff_i_etc_transposed_column_choices_witness_count_relation_bits)) * etc_row_scale_transposed_column_choices_witness)) /\ exists ff_q_etc_transposed_column_choices_witness_count_relation_bits_decoded. etc_row_code_transposed_column_choices_witness = ff_q_etc_transposed_column_choices_witness_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_choices_witness_count_relation_bits)) * etc_row_scale_transposed_column_choices_witness) + (ff_bit_etc_transposed_column_choices_witness_count_relation_bits))) /\ (ff_bit_etc_transposed_column_choices_witness_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_choices_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_choices_witness_inner_entry. ff_h_etc_transposed_column_choices_witness_inner_entry + S (etc_bit_transposed_column_choices) = S ((S (i)) * etc_row_scale_transposed_column_choices_witness)) /\ exists ff_q_etc_transposed_column_choices_witness_inner_entry. etc_row_code_transposed_column_choices_witness = ff_q_etc_transposed_column_choices_witness_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_choices_witness) + (etc_bit_transposed_column_choices))))))

Proof neighborhood

Direct theorem prerequisites

PA00E6 eisenstein_rectangle_decoded_row_count PA0029 beta_at_exists

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

37 script commands · 9 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)
beta at 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 bb
  6. L6
    intro bc
  7. L7
    intro i
  8. L8
    intro houter
  9. L9
    intro hi
  10. L10
    intro j
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hj
03Establish hrowL12–15

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

  1. L12
    have hrow : ∃ m. BetaAt(bb,bc,j,m) ∧ (∃ x. ∃ y. (∀ z. Lt(z,h) → ∃ n. BetaAt(x,y,z,n) ∧ (n = 0 ∧ (Lt(p · S j,q · S z) ∧ ¬Lt(q · S z,p · S j)) ∨ n = 1 ∧ (Lt(q · S z,p · S j) ∧ ¬Lt(p · S j,q · S z)))) ∧ BitCount(x,y,h,m))Definitions: BetaAt(bb,bc,j,m)Lt(z,h)BetaAt(x,y,z,n)Lt(p · S j,q · S z)Lt(q · S z,p · S j)BitCount(x,y,h,m)Original native command in the exact edition
  2. L13
    specialize houter j
  3. L14
    apply houter
  4. L15
    exact hj
04Separate the logical casesL16–20

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

  1. L16
    cases hrow
  2. L17
    cases hrow_witness
  3. L18
    cases hrow_witness_right
  4. L19
    cases hrow_witness_right_witness
  5. L20
    cases hrow_witness_right_witness_witness
05Establish hbitL21–25

Establish this local claim before using it. It is not an additional assumption.

  1. L21
    have hbit : ∃ d. BetaAt(x1,x2,i,d)Definitions: BetaAt(x1,x2,i,d)Original native command in the exact edition
  2. L22
    specialize beta_at_exists x1
  3. L23
    specialize beta_at_exists x2
  4. L24
    specialize beta_at_exists i
  5. L25
    exact beta_at_exists
06Separate the logical casesL26–26

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

  1. L26
    cases hbit
07Construct an explicit witnessL27–30

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

  1. L27
    exists x3
  2. L28
    exists x
  3. L29
    exists x1
  4. L30
    exists x2
08Separate the logical casesL31–33

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

  1. L31
    split
  2. L32
    split
  3. L33
    split
09Use earlier factsL34–37

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

  1. L34
    exact hrow_witness_left
  2. L35
    exact hrow_witness_right_witness_witness_left
  3. L36
    exact hrow_witness_right_witness_witness_right
  4. L37
    exact hbit_witness

Library-wide reading audit

Original defined command ledger · 37 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro i
  8. 0008intro houter
  9. 0009intro hi
  10. 0010intro j
  11. 0011intro hj
  12. 0012have hrow : ∃ m. BetaAt(bb,bc,j,m) ∧ (∃ x. ∃ y. (∀ z. Lt(z,h) → ∃ n. BetaAt(x,y,z,n) ∧ (n = 0 ∧ (Lt(p · S j,q · S z) ∧ ¬Lt(q · S z,p · S j)) ∨ n = 1 ∧ (Lt(q · S z,p · S j) ∧ ¬Lt(p · S j,q · S z)))) ∧ BitCount(x,y,h,m))
    Exact native replay linehave hrow : exists m. ((((exists ff_h_transposed_column_outer_entry. ff_h_transposed_column_outer_entry + S (m) = S ((S (j)) * bc)) /\ exists ff_q_transposed_column_outer_entry. bb = ff_q_transposed_column_outer_entry * S ((S (j)) * bc) + (m))) /\ (exists erc_row_code_transposed_column_outer_semantic erc_row_scale_transposed_column_outer_semantic. ((forall eri_column_erc_transposed_column_outer_semantic_row. (exists eri_gap_erc_transposed_column_outer_semantic_row_bound. eri_gap_erc_transposed_column_outer_semantic_row_bound + S (eri_column_erc_transposed_column_outer_semantic_row) = h) -> exists eri_bit_erc_transposed_column_outer_semantic_row. ((((exists ff_h_eri_erc_transposed_column_outer_semantic_row_decoded. ff_h_eri_erc_transposed_column_outer_semantic_row_decoded + S (eri_bit_erc_transposed_column_outer_semantic_row) = S ((S (eri_column_erc_transposed_column_outer_semantic_row)) * erc_row_scale_transposed_column_outer_semantic)) /\ exists ff_q_eri_erc_transposed_column_outer_semantic_row_decoded. erc_row_code_transposed_column_outer_semantic = ff_q_eri_erc_transposed_column_outer_semantic_row_decoded * S ((S (eri_column_erc_transposed_column_outer_semantic_row)) * erc_row_scale_transposed_column_outer_semantic) + (eri_bit_erc_transposed_column_outer_semantic_row))) /\ (((eri_bit_erc_transposed_column_outer_semantic_row = 0 /\ ((exists eri_gap_erc_transposed_column_outer_semantic_row_choice_left. eri_gap_erc_transposed_column_outer_semantic_row_choice_left + S (p * S j) = q * S eri_column_erc_transposed_column_outer_semantic_row) /\ ~(exists eri_gap_erc_transposed_column_outer_semantic_row_choice_right. eri_gap_erc_transposed_column_outer_semantic_row_choice_right + S (q * S eri_column_erc_transposed_column_outer_semantic_row) = p * S j))) \/ (eri_bit_erc_transposed_column_outer_semantic_row = 1 /\ ((exists eri_gap_erc_transposed_column_outer_semantic_row_choice_right. eri_gap_erc_transposed_column_outer_semantic_row_choice_right + S (q * S eri_column_erc_transposed_column_outer_semantic_row) = p * S j) /\ ~(exists eri_gap_erc_transposed_column_outer_semantic_row_choice_left. eri_gap_erc_transposed_column_outer_semantic_row_choice_left + S (p * S j) = q * S eri_column_erc_transposed_column_outer_semantic_row))))))) /\ (((exists ff_u_erc_transposed_column_outer_semantic_count_sum ff_v_erc_transposed_column_outer_semantic_count_sum. ((((exists ff_h_erc_transposed_column_outer_semantic_count_sum_start. ff_h_erc_transposed_column_outer_semantic_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_transposed_column_outer_semantic_count_sum)) /\ exists ff_q_erc_transposed_column_outer_semantic_count_sum_start. ff_u_erc_transposed_column_outer_semantic_count_sum = ff_q_erc_transposed_column_outer_semantic_count_sum_start * S ((S (0)) * ff_v_erc_transposed_column_outer_semantic_count_sum) + (0))) /\ ((((exists ff_h_erc_transposed_column_outer_semantic_count_sum_terminal. ff_h_erc_transposed_column_outer_semantic_count_sum_terminal + S (m) = S ((S (h)) * ff_v_erc_transposed_column_outer_semantic_count_sum)) /\ exists ff_q_erc_transposed_column_outer_semantic_count_sum_terminal. ff_u_erc_transposed_column_outer_semantic_count_sum = ff_q_erc_transposed_column_outer_semantic_count_sum_terminal * S ((S (h)) * ff_v_erc_transposed_column_outer_semantic_count_sum) + (m))) /\ forall ff_i_erc_transposed_column_outer_semantic_count_sum. (exists ff_lt_erc_transposed_column_outer_semantic_count_sum_bound. ff_lt_erc_transposed_column_outer_semantic_count_sum_bound + S ff_i_erc_transposed_column_outer_semantic_count_sum = h) -> exists ff_a_erc_transposed_column_outer_semantic_count_sum ff_r_erc_transposed_column_outer_semantic_count_sum ff_s_erc_transposed_column_outer_semantic_count_sum. ((((exists ff_h_erc_transposed_column_outer_semantic_count_sum_summand. ff_h_erc_transposed_column_outer_semantic_count_sum_summand + S (ff_a_erc_transposed_column_outer_semantic_count_sum) = S ((S (ff_i_erc_transposed_column_outer_semantic_count_sum)) * erc_row_scale_transposed_column_outer_semantic)) /\ exists ff_q_erc_transposed_column_outer_semantic_count_sum_summand. erc_row_code_transposed_column_outer_semantic = ff_q_erc_transposed_column_outer_semantic_count_sum_summand * S ((S (ff_i_erc_transposed_column_outer_semantic_count_sum)) * erc_row_scale_transposed_column_outer_semantic) + (ff_a_erc_transposed_column_outer_semantic_count_sum))) /\ ((((exists ff_h_erc_transposed_column_outer_semantic_count_sum_partial. ff_h_erc_transposed_column_outer_semantic_count_sum_partial + S (ff_r_erc_transposed_column_outer_semantic_count_sum) = S ((S (ff_i_erc_transposed_column_outer_semantic_count_sum)) * ff_v_erc_transposed_column_outer_semantic_count_sum)) /\ exists ff_q_erc_transposed_column_outer_semantic_count_sum_partial. ff_u_erc_transposed_column_outer_semantic_count_sum = ff_q_erc_transposed_column_outer_semantic_count_sum_partial * S ((S (ff_i_erc_transposed_column_outer_semantic_count_sum)) * ff_v_erc_transposed_column_outer_semantic_count_sum) + (ff_r_erc_transposed_column_outer_semantic_count_sum))) /\ ((((exists ff_h_erc_transposed_column_outer_semantic_count_sum_successor. ff_h_erc_transposed_column_outer_semantic_count_sum_successor + S (ff_s_erc_transposed_column_outer_semantic_count_sum) = S ((S (S ff_i_erc_transposed_column_outer_semantic_count_sum)) * ff_v_erc_transposed_column_outer_semantic_count_sum)) /\ exists ff_q_erc_transposed_column_outer_semantic_count_sum_successor. ff_u_erc_transposed_column_outer_semantic_count_sum = ff_q_erc_transposed_column_outer_semantic_count_sum_successor * S ((S (S ff_i_erc_transposed_column_outer_semantic_count_sum)) * ff_v_erc_transposed_column_outer_semantic_count_sum) + (ff_s_erc_transposed_column_outer_semantic_count_sum))) /\ ff_s_erc_transposed_column_outer_semantic_count_sum = ff_r_erc_transposed_column_outer_semantic_count_sum + ff_a_erc_transposed_column_outer_semantic_count_sum)))))) /\ (forall ff_i_erc_transposed_column_outer_semantic_count_bits. (exists ff_lt_erc_transposed_column_outer_semantic_count_bits_bound. ff_lt_erc_transposed_column_outer_semantic_count_bits_bound + S ff_i_erc_transposed_column_outer_semantic_count_bits = h) -> exists ff_bit_erc_transposed_column_outer_semantic_count_bits. ((((exists ff_h_erc_transposed_column_outer_semantic_count_bits_decoded. ff_h_erc_transposed_column_outer_semantic_count_bits_decoded + S (ff_bit_erc_transposed_column_outer_semantic_count_bits) = S ((S (ff_i_erc_transposed_column_outer_semantic_count_bits)) * erc_row_scale_transposed_column_outer_semantic)) /\ exists ff_q_erc_transposed_column_outer_semantic_count_bits_decoded. erc_row_code_transposed_column_outer_semantic = ff_q_erc_transposed_column_outer_semantic_count_bits_decoded * S ((S (ff_i_erc_transposed_column_outer_semantic_count_bits)) * erc_row_scale_transposed_column_outer_semantic) + (ff_bit_erc_transposed_column_outer_semantic_count_bits))) /\ (ff_bit_erc_transposed_column_outer_semantic_count_bits = 0 \/ ff_bit_erc_transposed_column_outer_semantic_count_bits = 1))))))))
  13. 0013specialize houter j
  14. 0014apply houter
  15. 0015exact hj
  16. 0016cases hrow
  17. 0017cases hrow_witness
  18. 0018cases hrow_witness_right
  19. 0019cases hrow_witness_right_witness
  20. 0020cases hrow_witness_right_witness_witness
  21. 0021have hbit : ∃ d. BetaAt(x1,x2,i,d)
    Exact native replay linehave hbit : exists d. (((exists ff_h_transposed_column_choice_bit. ff_h_transposed_column_choice_bit + S (d) = S ((S (i)) * x2)) /\ exists ff_q_transposed_column_choice_bit. x1 = ff_q_transposed_column_choice_bit * S ((S (i)) * x2) + (d)))
  22. 0022specialize beta_at_exists x1
  23. 0023specialize beta_at_exists x2
  24. 0024specialize beta_at_exists i
  25. 0025exact beta_at_exists
  26. 0026cases hbit
  27. 0027exists x3
  28. 0028exists x
  29. 0029exists x1
  30. 0030exists x2
  31. 0031split
  32. 0032split
  33. 0033split
  34. 0034exact hrow_witness_left
  35. 0035exact hrow_witness_right_witness_witness_left
  36. 0036exact hrow_witness_right_witness_witness_right
  37. 0037exact hbit_witness