PA00E7

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.

Exact expanded 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))))))

Structural proof guide

Generated structural guide

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

Use the direct prerequisites eisenstein_rectangle_decoded_row_count, beta_at_exists as previously established PA formulas.

The proof proceeds by case analysis (6), intermediate claims (2).

Referenced ingredients

PA00E6 eisenstein_rectangle_decoded_row_count PA0029 beta_at_exists

Proof neighborhood

Direct dependencies

PA00E6 eisenstein_rectangle_decoded_row_count PA0029 beta_at_exists

Direct dependents

PA00EF eisenstein_row_transposed_column_count_partition PA00F7 eisenstein_fubini_column_count_witness_retarget

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

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.

Named ingredients (1)
beta at exists

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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: LtBetaAtBitCount
  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 : 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)))
  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 exact 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 : 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 : 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